Commits

Branch selector

 master

User selector

All users

All time

Commit History

Commits on Feb 1, 2016

• Update paper status

  jinala

  committed
  55d3ddf

  Copy full SHA for 55d3ddf

Commits on Jan 13, 2016

• Lemma cache datatypes. Do not send true lemma in quantifiers. Minor fix for datatypes model generation for UFinite datatypes when FMF.

  ajreynol

  committed
  94fe6a0

  Copy full SHA for 94fe6a0

Commits on Jan 9, 2016

• Adding a new Listener utility class. Changing the ResourceManager to use Listeners for reporting hard and soft resource out() events.

  timothy-king

  committed
  3a973bd

  Copy full SHA for 3a973bd

• Removing StatisticsRegistry's static functions current() and registerStat().

  Show description for f4ef7af
  timothy-king

  committed
  f4ef7af

  Copy full SHA for f4ef7af

Commits on Jan 8, 2016

• Disabling the RESTART command.

  timothy-king

  committed
  def0a07

  Copy full SHA for def0a07

Commits on Jan 6, 2016

• fix windows builds

  kbansal

  committed
  3a78a63

  Copy full SHA for 3a78a63

• Fixing a SWIG ordering issue between bitvector and integer.

  timothy-king

  committed
  62dc798

  Copy full SHA for 62dc798

• Improving the documentation of the CVC command CONTINUE.

  timothy-king

  committed
  d0ef178

  Copy full SHA for d0ef178

• Removing dead code. StackingMap only appeared in unit tests.

  timothy-king

  committed
  774af8c

  Copy full SHA for 774af8c

• Moving sexpr.{cpp,h,i} from expr/ back into util/.

  timothy-king

  committed
  b5f91da

  Copy full SHA for b5f91da

• Add SmtGlobals Class

  Show description for 5eabda0
  timothy-king

  committed
  5eabda0

  Copy full SHA for 5eabda0

Commits on Jan 5, 2016

• Adding a new class LastExceptionBuffer for the purpose of owning the memory for the last exception C string. This replaces s_debugLastException.

  timothy-king

  committed
  b717513

  Copy full SHA for b717513

Commits on Jan 1, 2016

• Added propagation rule for array ext lemmas to aid proofs

  barrettcw

  committed
  541c88a

  Copy full SHA for 541c88a

Commits on Dec 31, 2015

• Modified tear-down-incremental option to take an integer - the integer is the

  Show description for 395e05c
  barrettcw

  committed
  395e05c

  Copy full SHA for 395e05c

Commits on Dec 30, 2015

• Shuffling around public vs. private headers

  Show description for fa7f30a
  timothy-king

  committed
  fa7f30a

  Copy full SHA for fa7f30a

Commits on Dec 29, 2015

• Adding a missing header include for cvc4_assert.h in smt_engine_check_proof.cpp for when proofs are disabled.

  timothy-king

  committed
  1ce3971

  Copy full SHA for 1ce3971

Commits on Dec 27, 2015

• Merged my changes from experimental branch (new array decision procedure,

  Show description for 815f2c9
  barrettcw

  committed
  815f2c9

  Copy full SHA for 815f2c9

Commits on Dec 24, 2015

• Changing the attribute on the forward declaration of SetType in emptyset.h. This seems to give many fewer warnings.

  timothy-king

  committed
  36eb9ee

  Copy full SHA for 36eb9ee

• Adding a missing return on the new ArrayStoreAll::operator= .

  timothy-king

  committed
  e9a8aee

  Copy full SHA for e9a8aee

• Miscellaneous fixes

  Show description for a39ad65
  timothy-king

  committed
  a39ad65

  Copy full SHA for a39ad65

Commits on Dec 23, 2015

• Enabled array propagation during lemma propagation - this should catch some

  Show description for 87b0fe9
  barrettcw

  committed
  87b0fe9

  Copy full SHA for 87b0fe9

• Added extract.cpp example

  barrettcw

  committed
  0879991

  Copy full SHA for 0879991

Commits on Dec 22, 2015

• Bug fix uf-ss-totality.

  ajreynol

  committed
  eb97dc0

  Copy full SHA for eb97dc0

• Always split on constructor types for datatypes involving uninterpreted sorts when finite model finding is enabled, add regressions.

  ajreynol

  committed
  75003d9

  Copy full SHA for 75003d9

• Bug fix for cbqi, do not use model values for terms involving non-enumerable sorts.

  ajreynol

  committed
  bd6a13b

  Copy full SHA for bd6a13b

Commits on Dec 19, 2015

• Modifying emptyset.h and sexpr. Adding SetLanguage.

  Show description for 5f207ba
  timothy-king

  committed
  5f207ba

  Copy full SHA for 5f207ba

Commits on Dec 17, 2015

• Minor

  ajreynol

  committed
  7e4468b

  Copy full SHA for 7e4468b

Commits on Dec 16, 2015

• Removing the Record iterator from the swig interface. Moving the cvc4 autogen include in interactive_shell.cpp.

  timothy-king

  committed
  a0c5d25

  Copy full SHA for a0c5d25

• Work on purification for quantifiers, minor updates.

  ajreynol

  committed
  b224649

  Copy full SHA for b224649

Commits on Dec 15, 2015

• Breaking the include cycle between Record and Expr.

  timothy-king

  committed
  3f29ad7

  Copy full SHA for 3f29ad7

• Adding destructors for CDO an CDOhash_map in the restore() functions.

  timothy-king

  committed
  c358ccb

  Copy full SHA for c358ccb

• Removing the build cycle for predicate.

  timothy-king

  committed
  b812dec

  Copy full SHA for b812dec

• Moving SExpr(bool) out of the header into sexpr.cpp to be less verbose about the warning.

  timothy-king

  committed
  b66c195

  Copy full SHA for b66c195

• Making logic_info_forward.h a public header for now.

  timothy-king

  committed
  3792dfc

  Copy full SHA for 3792dfc

• Add option uf-ss-fair-monotone. Minor cleanup and improvement of sort inference.

  ajreynol

  committed
  e600773

  Copy full SHA for e600773