cvc5.git
12 years ago* improving arithmetic getEqualityStatus
Dejan Jovanović [Thu, 22 Mar 2012 23:09:03 +0000 (23:09 +0000)]
* improving arithmetic getEqualityStatus
* some sharing improvements based on model

12 years agoMerged updated version of the bitvector theory:
Liana Hadarean [Thu, 22 Mar 2012 21:45:31 +0000 (21:45 +0000)]
Merged updated version of the bitvector theory:
  * added simplification rewrites

12 years agosome improvements to the sharing mechanism/interface
Dejan Jovanović [Thu, 22 Mar 2012 20:40:41 +0000 (20:40 +0000)]
some improvements to the sharing mechanism/interface

12 years agoDisable nonclausal simplification for QF_SAT benchmarks by default.
Morgan Deters [Wed, 21 Mar 2012 20:51:02 +0000 (20:51 +0000)]
Disable nonclausal simplification for QF_SAT benchmarks by default.
(Can be overridden with --simplification=batch, for example.)

12 years agoSome work on the dump infrastructure to support portfolio work.
Morgan Deters [Fri, 9 Mar 2012 21:10:17 +0000 (21:10 +0000)]
Some work on the dump infrastructure to support portfolio work.

  Dump("foo") << FooCommand(...);

now "dumps" the textual representation of the command (in the current
output language) to a file, IF dumping is on at configure-time, AND the
"muzzle" feature is off, AND the "foo" flag is turned on for the dump
stream during this run.

If it's a portfolio build, the above will also store the command in a
CommandSequence, IF the "foo" flag is turned on for the dump stream
during this run.  This is done even if the muzzle is on.

This commit also cleans up some code that used the dump feature (in arrays,
particularly).

12 years agofix a "lost command" bug and associated memory leak in SMT-LIBv1 parser due to an...
Morgan Deters [Fri, 9 Mar 2012 21:00:51 +0000 (21:00 +0000)]
fix a "lost command" bug and associated memory leak in SMT-LIBv1 parser due to an out-of-place parenthesis

12 years agoStrengthen minisat assertion regarding t-propagations that was unintentionally allowi...
Morgan Deters [Fri, 9 Mar 2012 20:30:15 +0000 (20:30 +0000)]
Strengthen minisat assertion regarding t-propagations that was unintentionally allowing a theory to propagate p and ~p at the same time (and the conflict was undetected, leading to an incorrect answer).  Credit to Clark for finding this.

12 years agominor fixes: to "make dist" in build directories with language bindings enabled;...
Morgan Deters [Fri, 9 Mar 2012 18:26:07 +0000 (18:26 +0000)]
minor fixes: to "make dist" in build directories with language bindings enabled; and to makefile standards conformance

12 years agofix "make dist"
Morgan Deters [Thu, 8 Mar 2012 19:06:08 +0000 (19:06 +0000)]
fix "make dist"

12 years agoFixin the bug Clark found. In final check, enqueued propagations were not discharged.
Dejan Jovanović [Thu, 8 Mar 2012 18:54:02 +0000 (18:54 +0000)]
Fixin the bug Clark found. In final check, enqueued propagations were not discharged.

12 years agoRemoving QUICK_CHECK, and other unused ones, from the Theory::Effort.
Dejan Jovanović [Thu, 8 Mar 2012 02:33:37 +0000 (02:33 +0000)]
Removing QUICK_CHECK, and other unused ones, from the Theory::Effort.

Seems to be working better <http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3749&category=&p=5&reference_id=3739>, and should fix the failing cases in the regressions.

Removing one test case from the integer regress0.

12 years agocdqueue : fix size(). Thank you Clark for spotting this silly mistake.
François Bobot [Wed, 7 Mar 2012 22:29:39 +0000 (22:29 +0000)]
cdqueue : fix size(). Thank you Clark for spotting this silly mistake.

12 years agofix some Java compatibility-layer interface problems; also fix some Mac OS X build...
Morgan Deters [Wed, 7 Mar 2012 21:38:04 +0000 (21:38 +0000)]
fix some Java compatibility-layer interface problems; also fix some Mac OS X build issues

12 years agoupdating the equality engine to be able to give explanations for terms that were...
Dejan Jovanović [Tue, 6 Mar 2012 19:08:32 +0000 (19:08 +0000)]
updating the equality engine to be able to give explanations for terms that were not in the databas (queried by areEqual and areDisequal)
and it's a bit better
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3738&category=&p=-1&reference_id=3731

12 years agoChanging the dependency checking; GMP is required (and sometimes must be explicitly...
Morgan Deters [Sat, 3 Mar 2012 23:29:20 +0000 (23:29 +0000)]
Changing the dependency checking; GMP is required (and sometimes must be explicitly linked in with -l) when using CLN.  Fixes a bug on recent Debian that Francois reported.  Hopefully this doesn't break anything..

12 years agoRemove some commented out code from sat.h
Kshitij Bansal [Fri, 2 Mar 2012 23:43:50 +0000 (23:43 +0000)]
Remove some commented out code from sat.h

12 years agoThis commit merges in the changes from branches/arithmetic/refactor0
Tim King [Fri, 2 Mar 2012 23:37:06 +0000 (23:37 +0000)]
This commit merges in the changes from branches/arithmetic/refactor0
- Improved the checks in AssertLower and AssertUpper so that redundant bounds cause less work.
- Because of the above change, d_constantIntegerVariables now cannot have duplicate elements enqueued. This allows removing d_varsInDioSolver.
- Fix to an assertion in CDQueue.
- Implements a CDArithVarSet using a vector of booleans and CDList.
- Refactored ArithVar out of arith_utilities.h. Miscellaneous cleanup of arithmetic.

12 years agoCDMap -> CDHashMap
Dejan Jovanović [Fri, 2 Mar 2012 20:38:23 +0000 (20:38 +0000)]
CDMap -> CDHashMap
CDSet -> CDHashSet

12 years agocommitting the TNode/Node fix that was in the kind-backend branch; there's still...
Morgan Deters [Fri, 2 Mar 2012 20:12:44 +0000 (20:12 +0000)]
committing the TNode/Node fix that was in the kind-backend branch; there's still something fishy here, I think I need to merge in a few more things to support incrementality properly.  But this fixes "make check" for now

12 years agoRenamed CDQueue to CDTrailQueue and CDQueue2 to CDQueue. Small changes to function...
Tim King [Fri, 2 Mar 2012 16:32:16 +0000 (16:32 +0000)]
Renamed CDQueue to CDTrailQueue and CDQueue2 to CDQueue. Small changes to function names and documentation.

12 years agoPartial merge from kind-backend branch, including Minisat and CNF work to
Morgan Deters [Thu, 1 Mar 2012 14:48:04 +0000 (14:48 +0000)]
Partial merge from kind-backend branch, including Minisat and CNF work to
support incrementality.

Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.

Expected performance change negligible; slightly better on memory:
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!

12 years agocdqueue2 : cdlist that can be used like queue and can delete element that will never...
François Bobot [Thu, 1 Mar 2012 01:34:35 +0000 (01:34 +0000)]
cdqueue2 : cdlist that can be used like queue and can delete element that will never be restored

12 years agoFixed a copy paste error where a lower bound was looked up instead of an upper bound.
Tim King [Thu, 1 Mar 2012 00:38:37 +0000 (00:38 +0000)]
Fixed a copy paste error where a lower bound was looked up instead of an upper bound.

12 years agoThis should fix the debian build fails:
Liana Hadarean [Wed, 29 Feb 2012 20:33:43 +0000 (20:33 +0000)]
This should fix the debian build fails:
   * removed bvpicosat directory as it is currently not used

Cleared some of the flurry of warnings my previous merge caused in src/prop/

12 years agofixing bug310
Dejan Jovanović [Wed, 29 Feb 2012 20:06:21 +0000 (20:06 +0000)]
fixing bug310

* theories that are parametric and therefore need the combination framwork should be tagged as "parametric" in the kinds file
* default care graph computation was not sufficient, fixed

12 years agoconsistency in how the Dump output stream is used
Morgan Deters [Wed, 29 Feb 2012 17:49:44 +0000 (17:49 +0000)]
consistency in how the Dump output stream is used

12 years agoThis commit merges in branches/arithmetic/internalbb up to revision 2831. This is...
Tim King [Tue, 28 Feb 2012 21:26:35 +0000 (21:26 +0000)]
This commit merges in branches/arithmetic/internalbb up to revision 2831.  This is a significant refactoring of code.

- r2820
-- Refactors Simplex so that it does significantly fewer functions.
--  Adds the LinearEqualityModule for handling update and pivotAndUpdate and other utility functions that require access to both the tableau and partial model.
-- Some of the code for propagation has moved to TheoryArith.
-r2826
-- Small changes to documentation and removes the no longer implemented deduceLowerBound() and deduceUpperBound().
- r2827
-- Adds isZero() to Rational. Adds cmp to DeltaRational.
- r2831
-- Refactored comparison to upper and lower in the partial model to use DeltaRational::cmp.
-- Refactored AssertUpper and AssertLower in TheoryArith to include functionality that has weaseled into TheoryArith::assertionCases.

12 years agoImproves the arithmetic difference manager to delay any work until a shared term...
Tim King [Tue, 28 Feb 2012 20:42:55 +0000 (20:42 +0000)]
Improves the arithmetic difference manager to delay any work until a shared term is added.

12 years agofix theory "kinds" file documentation for allowed arity of operators
Morgan Deters [Tue, 28 Feb 2012 20:20:03 +0000 (20:20 +0000)]
fix theory "kinds" file documentation for allowed arity of operators

12 years agoAdds the CDQueue class. This is a wrapper for combining a CDList<T> and a CDO<size_t...
Tim King [Tue, 28 Feb 2012 20:13:02 +0000 (20:13 +0000)]
Adds the CDQueue class.  This is a wrapper for combining a CDList<T> and a CDO<size_t> into a FIFO queue.

12 years agoReplace the sequence of hardcoded addTheory() calls with a use of the theory traits...
Morgan Deters [Tue, 28 Feb 2012 19:51:10 +0000 (19:51 +0000)]
Replace the sequence of hardcoded addTheory() calls with a use of the theory traits---with the effect that everything with a kinds file is registered as a theory.  Eventually we may want a more dynamic way of selecting theory implementations, but for now we don't have a need for this.  Expected performance impact: none.  (This commit addresses and re-closes the reopened bug #307.)

12 years agofixes to new-theory script; resolves bug #307
Morgan Deters [Mon, 27 Feb 2012 22:51:53 +0000 (22:51 +0000)]
fixes to new-theory script; resolves bug #307

12 years agoppAsert -> ppAssert
Dejan Jovanović [Sat, 25 Feb 2012 22:35:53 +0000 (22:35 +0000)]
ppAsert -> ppAssert

12 years agoRefactored CnfStream to work with the bv theory Bitblaster:
Liana Hadarean [Sat, 25 Feb 2012 18:23:10 +0000 (18:23 +0000)]
Refactored CnfStream to work with the bv theory Bitblaster:
    * separated SatSolverInput interface class into two classes:
           - TheoryProxy for the sat solver to communicate with the theories
           - SatSolverInterface abstract class to communicate with the sat solver
    * instead of using #ifdef typedef for SatClauses and SatLiterals, now there are CVC4 SatLiteral/SatClause types and mappings between them and the internal sat solver clause/literal representation
    * added abstract classes for DPLLSatSolver and BVSatSolver different interfaces

Replaced TheoryBV with bitblasting implementation:
    * all operators bitblasted
    * only operator elimination rewrite rules so far

12 years agoTheory interface changes:
Dejan Jovanović [Fri, 24 Feb 2012 20:29:12 +0000 (20:29 +0000)]
Theory interface changes:

solve -> ppAsert
staticLearning -> ppStaticLearn
preprocess -> ppRewrite
SolveStatus -> PPAssertStatus (SOLVE_* -> PP_ASSERT_*)

via Eclipse refactoring magic.

12 years agoAdded ability to set a "cvc4-specific logic" in standards-compliant
Morgan Deters [Thu, 23 Feb 2012 23:08:03 +0000 (23:08 +0000)]
Added ability to set a "cvc4-specific logic" in standards-compliant
SMT-LIBv1 and SMT-LIBv2 input:

    In SMT-LIBv1, you specify the "cvc4_logic" benchmark attribute; for instance:

    (benchmark actually_a_sat_benchmark_but_looks_like_uf
      :logic QF_UF
      :cvc4_logic { QF_SAT }
      [...]

    In SMT-LIBv2, you use a set-info; for instance:

    (set-logic QF_UF)
    (set-info :cvc4-logic "QF_SAT")
    [...]

    Right now, the only thing this does is disable the symmetry breaker for
    benchmarks like the above ones.

As part of this work, TheoryEngine::setLogic() was removed (the logic field there
wasn't actually used anywhere, its need disappeared when
Theory::setUninterpretedSortOwner() was provided).

Also, Theory::d_uninterpretedSortOwner got a name change to
Theory::s_uninterpretedSortOwner, to highlight that it is static to the Theory
class.  This represents a breakage of our separation goals for CVC4, since it
means that two SmtEngines cannot be created separately to solve a QF_AX and
QF_UF problem.  A bug report is pending.

12 years agopcvc4 only built if --with-portfolio given to the configure script (Clark-requested...
Morgan Deters [Thu, 23 Feb 2012 22:02:45 +0000 (22:02 +0000)]
pcvc4 only built if --with-portfolio given to the configure script (Clark-requested change)

12 years agoFix for bug 305.
Tim King [Wed, 22 Feb 2012 22:32:45 +0000 (22:32 +0000)]
Fix for bug 305.

12 years agofixes to configure and boost.m4 to make certain boost installations nonfatal errors...
Morgan Deters [Wed, 22 Feb 2012 22:24:19 +0000 (22:24 +0000)]
fixes to configure and boost.m4 to make certain boost installations nonfatal errors; threading support should only be required to build pcvc4, not cvc4

12 years agoanother static library unavailability issue
Morgan Deters [Wed, 22 Feb 2012 20:36:15 +0000 (20:36 +0000)]
another static library unavailability issue

12 years agomake sure to clear out READLINE_LIBS if readline causes problems at configure time...
Morgan Deters [Wed, 22 Feb 2012 20:12:44 +0000 (20:12 +0000)]
make sure to clear out READLINE_LIBS if readline causes problems at configure time; fixes a bug reported by Clark for static-binary builds on machines where no static libreadline is available (like CIMS machines)

12 years agoAdded OutputChannel::propagateAsDecision() functionality, allowing a theory
Morgan Deters [Wed, 22 Feb 2012 20:08:57 +0000 (20:08 +0000)]
Added OutputChannel::propagateAsDecision() functionality, allowing a theory
to request a decision on a literal.  All these theory requests are kept in a
context-dependent queue and serviced in order when the SAT solver goes to make a
decision.  Requests that don't have a SAT literal give an assert-fail.  Requests
for literals that already have an assignment are silently ignored.

Since the queue is CD, requests can actually be serviced more than once (e.g., if
a request is made at DL 5, but not serviced until DL 10, and later, a conflict
backtracks to level 7, the request may be serviced again).

Performance impact: none to negligible for theories that don't use it
  See http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3620&reference_id=3614&mode=&category=&p=0

12 years agoFixes to documentation / fixes for MacOS
Morgan Deters [Wed, 22 Feb 2012 15:30:51 +0000 (15:30 +0000)]
Fixes to documentation / fixes for MacOS

12 years agominor change to order fn in sat solver's ElimLt
Kshitij Bansal [Wed, 22 Feb 2012 03:00:24 +0000 (03:00 +0000)]
minor change to order fn in sat solver's ElimLt
(better, (marginally) faster -- regressions 3605, 3606)

12 years agoadd a "--with-portfolio" configure option that makes a missing boost-thread library...
Morgan Deters [Tue, 21 Feb 2012 23:02:23 +0000 (23:02 +0000)]
add a "--with-portfolio" configure option that makes a missing boost-thread library an error; useful for builds requiring a "pcvc4" binary at the end

12 years agofix src/util/hash.h to specialize GNU's hash template for <uint64_t> on platforms...
Morgan Deters [Tue, 21 Feb 2012 22:13:05 +0000 (22:13 +0000)]
fix src/util/hash.h to specialize GNU's hash template for <uint64_t> on platforms that need it; fixes Mac builds.

12 years agolanguage bindings fixes for yesterday's portfolio merge
Morgan Deters [Tue, 21 Feb 2012 21:52:17 +0000 (21:52 +0000)]
language bindings fixes for yesterday's portfolio merge

12 years agoFix for bug303. The problem was with function applications that get normalized when...
Dejan Jovanović [Tue, 21 Feb 2012 19:43:46 +0000 (19:43 +0000)]
Fix for bug303. The problem was with function applications that get normalized when added to the term database. For example, if x=y exists, and the term f(x) is added, f(y) was stored. So, when getExplanation(f(x), f(y)) was called, trouble ensued. I now keep the original version so that explanations can be properly produced.

Also added theory::assertions debug flag that will printout assertions of each theory for ease and uniformity of debugging in the future.

12 years agodon't require libboost_thread (its presence is detected at configure-time), and other...
Morgan Deters [Tue, 21 Feb 2012 19:24:51 +0000 (19:24 +0000)]
don't require libboost_thread (its presence is detected at configure-time), and other build/documentation fixes from yesterday's portfolio merge; resolves bug 302

12 years agofix sharing issue for portfolio (full lit-to-node map wasn't being kept in my previou...
Morgan Deters [Mon, 20 Feb 2012 20:04:31 +0000 (20:04 +0000)]
fix sharing issue for portfolio (full lit-to-node map wasn't being kept in my previous checkin)

12 years agofix "make dist"
Morgan Deters [Mon, 20 Feb 2012 18:23:15 +0000 (18:23 +0000)]
fix "make dist"

12 years agozlib not required; remove configure's dependency on it
Morgan Deters [Mon, 20 Feb 2012 18:22:27 +0000 (18:22 +0000)]
zlib not required; remove configure's dependency on it

12 years agoportfolio merge
Morgan Deters [Mon, 20 Feb 2012 17:59:33 +0000 (17:59 +0000)]
portfolio merge

12 years agoreadline links in -ltermcap -ltinfo too (fixes breakage in static-binary builds)
Morgan Deters [Mon, 20 Feb 2012 16:28:44 +0000 (16:28 +0000)]
readline links in -ltermcap -ltinfo too (fixes breakage in static-binary builds)

12 years agoAdded Theory::postsolve() infrastructure as Clark requested.
Morgan Deters [Mon, 20 Feb 2012 14:48:22 +0000 (14:48 +0000)]
Added Theory::postsolve() infrastructure as Clark requested.
(Though currently unused.)

For theories that request presolve and postsolve (in their kinds file),
they will get a presolve() notification before the first check().  After
the final check during the current search, they get a postsolve().
presolve() and postsolve() notifications always come in pairs, bracketing
all check()/propagate()/getValue() calls related to a single query.  In
the case of incremental benchmarks, theories may get additional
presolve()/postsolve() pairs, but again, they always come in pairs.

Expected performance impact: none (for theories that don't use it)
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3598&reference_id=3581&p=5

12 years agoBy default, ONLY enable symmetry breaker ONLY for QF_UF (both SMT-LIBv1
Morgan Deters [Mon, 20 Feb 2012 13:44:50 +0000 (13:44 +0000)]
By default, ONLY enable symmetry breaker ONLY for QF_UF (both SMT-LIBv1
and SMT-LIBv2).

There are --enable-symmetry-breaker and --disable-symmetry-breaker
options that are always respected regardless of this default.

Expected performance impact: positive

New default (UF only) compared to old default (always on):
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3594&reference_id=3595&p=5

Symmetry breaker remains a big win on UF:
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3594&reference_id=3596&p=5

The last link to results looks at first that the symmetry breaker should
always be turned off, since its use loses more regressions than it gains.
*However*, the lost ones are only our "QF_SAT" benchmarks.  For these, we
should indeed turn off the symmetry breaker, but that's impossible for
now because we tag them internally with the logic "QF_UF."

12 years agoclarify wording in README, thanks for finding this Francois!
Morgan Deters [Thu, 16 Feb 2012 13:30:28 +0000 (13:30 +0000)]
clarify wording in README, thanks for finding this Francois!

12 years agoLast commit accidentally lacked r2778 and r2779 from integer2. I have manually broug...
Tim King [Thu, 16 Feb 2012 00:54:12 +0000 (00:54 +0000)]
Last commit accidentally lacked r2778 and r2779 from integer2.  I have manually brought these changes over.  Changed the tests used by test/regress/regress0/arith/integers/Makefile.am to be 15 of the more interesting tests.  Did a bit of cleanup on TheoryArith to eliminate a warning and remove dead code.

12 years agoThis commit merges into trunk the branch branches/arithmetic/integers2 from r2650...
Tim King [Wed, 15 Feb 2012 21:52:16 +0000 (21:52 +0000)]
This commit merges into trunk the branch branches/arithmetic/integers2 from r2650 to r2779.
- This excludes revision 2777.  This revision had some strange performance implications and was delaying the merge.
- This includes the new DioSolver. The DioSolver can discover conflicts, produce substitutions, and produce cuts.
- The DioSolver can be disabled at command line using --disable-dio-solver.
- This includes a number of changes to the arithmetic normal form.
- The Integer class features a number of new number theoretic function.
- This commit includes a few rather loud warning. I will do my best to take care of them today.

12 years agoprecision in theoryskel
François Bobot [Mon, 13 Feb 2012 23:12:15 +0000 (23:12 +0000)]
precision in theoryskel

12 years agoproper handling of improper get-value
Morgan Deters [Mon, 13 Feb 2012 01:06:01 +0000 (01:06 +0000)]
proper handling of improper get-value

12 years agocopyright year updated to 2012
Morgan Deters [Sun, 12 Feb 2012 22:01:47 +0000 (22:01 +0000)]
copyright year updated to 2012

12 years agoseparate new-theory components into a "theoryskel" directory so that new files can...
Morgan Deters [Sun, 12 Feb 2012 20:59:13 +0000 (20:59 +0000)]
separate new-theory components into a "theoryskel" directory so that new files can be added to it without modifying the script.

12 years agoensure using bash for new-theory script
Morgan Deters [Sat, 11 Feb 2012 21:57:14 +0000 (21:57 +0000)]
ensure using bash for new-theory script

12 years agoattempt at a fix for the local regression failure (CLN linking issues on oneiric
Morgan Deters [Fri, 10 Feb 2012 23:43:06 +0000 (23:43 +0000)]
attempt at a fix for the local regression failure (CLN linking issues on oneiric

12 years agoscript to ease creating a new theory from scratch (will go along with new reference...
Morgan Deters [Fri, 10 Feb 2012 23:36:07 +0000 (23:36 +0000)]
script to ease creating a new theory from scratch (will go along with new reference documentation)

12 years agocorrect comment typo found during today's architectural meeting
Morgan Deters [Fri, 10 Feb 2012 20:27:10 +0000 (20:27 +0000)]
correct comment typo found during today's architectural meeting

12 years agofixing antoher small bug in backtracking
Dejan Jovanović [Thu, 9 Feb 2012 21:25:00 +0000 (21:25 +0000)]
fixing antoher small bug in backtracking

12 years agofixing a bug in uf_engine application lookup backtracking
Dejan Jovanović [Wed, 8 Feb 2012 16:04:24 +0000 (16:04 +0000)]
fixing a bug in uf_engine application lookup backtracking
this should also fix bug299

12 years agoNumber of changes to cvc_printer.cpp. Specialized the printing for BVPLUS, BVSUB...
Tim King [Wed, 8 Feb 2012 00:31:00 +0000 (00:31 +0000)]
Number of changes to cvc_printer.cpp. Specialized the printing for BVPLUS, BVSUB, and BVMULT.  Fixed a bug in printing on PREFIX operators. Added parenthsis for POSTFIX operators. Passing the ouroborous test now.

12 years agore-adding comment about available languages
Morgan Deters [Tue, 7 Feb 2012 22:13:12 +0000 (22:13 +0000)]
re-adding comment about available languages

12 years agoremoving the 100 integer benchmarks from regress0, too many
Dejan Jovanović [Tue, 7 Feb 2012 16:20:52 +0000 (16:20 +0000)]
removing the 100 integer benchmarks from regress0, too many

12 years agofixing some missing stuff
Dejan Jovanović [Tue, 7 Feb 2012 16:14:17 +0000 (16:14 +0000)]
fixing some missing stuff

12 years agoFixing a bug in the integer unit tests when configured for GMP with assertions off.
Tim King [Mon, 6 Feb 2012 18:32:52 +0000 (18:32 +0000)]
Fixing a bug in the integer unit tests when configured for GMP with assertions off.

12 years agochanges to the cvc4 language printer, so that it actually prints the cvc4 language
Dejan Jovanović [Sun, 5 Feb 2012 21:44:02 +0000 (21:44 +0000)]
changes to the cvc4 language printer, so that it actually prints the cvc4 language
all theory writers should take a look a what's being printed, to ensure all cases are covered

12 years agosupport for isWellFounded/mkGroundTerm on uninterpretted sorts. cvc4 now assumes...
Andrew Reynolds [Sat, 4 Feb 2012 22:19:12 +0000 (22:19 +0000)]
support for isWellFounded/mkGroundTerm on uninterpretted sorts.  cvc4 now assumes uninterpretted sorts are well-founded, allowing datatypes to work with uninterpretted sort subdata

12 years agoupdating configure to use python-config for building python bindings
Dejan Jovanović [Fri, 3 Feb 2012 23:17:30 +0000 (23:17 +0000)]
updating configure to use python-config for building python bindings

12 years agoeffecting the same change in the compat Java binding as was done to CVC3 yesterday...
Morgan Deters [Fri, 27 Jan 2012 20:00:54 +0000 (20:00 +0000)]
effecting the same change in the compat Java binding as was done to CVC3 yesterday (ValidityChecker::value() and ValidityChecker::getValue())

12 years agoAdding regress1 test ooo.rf6.smt2.
Tim King [Wed, 25 Jan 2012 16:36:19 +0000 (16:36 +0000)]
Adding regress1 test ooo.rf6.smt2.

12 years agoPartial fix to TheoryEngine::getExplanation so that SharedAssertions request explanat...
Tim King [Mon, 23 Jan 2012 21:13:08 +0000 (21:13 +0000)]
Partial fix to TheoryEngine::getExplanation so that SharedAssertions request explanations from the theory that can explain them. This partially fixes bug 295.

12 years agofix for bug295
Dejan Jovanović [Mon, 23 Jan 2012 04:19:38 +0000 (04:19 +0000)]
fix for bug295

12 years agoupdates to smt2 parser to support datatypes, minor updates to datatypes theory/rewrit...
Andrew Reynolds [Tue, 17 Jan 2012 18:15:03 +0000 (18:15 +0000)]
updates to smt2 parser to support datatypes, minor updates to datatypes theory/rewriter to support datatypes with non-datatype subdata

12 years agoPartial fix to bug 295.
Tim King [Thu, 15 Dec 2011 22:23:25 +0000 (22:23 +0000)]
Partial fix to bug 295.

12 years agoFix to the previous commit.
Tim King [Thu, 15 Dec 2011 21:02:33 +0000 (21:02 +0000)]
Fix to the previous commit.

12 years agoPartial fix in arithmetic for propagating shared terms. This partially resolves bug...
Tim King [Thu, 15 Dec 2011 20:39:20 +0000 (20:39 +0000)]
Partial fix in arithmetic for propagating shared terms. This partially resolves bug 289.  Adds failing tests to regress1.

12 years agoadded minor documentation for parametric datatypes, for bug 283
Andrew Reynolds [Wed, 14 Dec 2011 23:40:44 +0000 (23:40 +0000)]
added minor documentation for parametric datatypes, for bug 283

12 years agominor fixes to printing and parsing of CVC-language defined functions and lambdas...
Morgan Deters [Wed, 14 Dec 2011 22:44:58 +0000 (22:44 +0000)]
minor fixes to printing and parsing of CVC-language defined functions and lambdas; resolves bug 294

12 years agosome more bug fixes (TNode -> Node, normalize literals in explanations)
Dejan Jovanović [Wed, 14 Dec 2011 09:31:21 +0000 (09:31 +0000)]
some more bug fixes (TNode -> Node, normalize literals in explanations)

12 years ago* merging some uf stuff from incremental_work branch that somehow nobody merged-in
Dejan Jovanović [Mon, 12 Dec 2011 09:47:37 +0000 (09:47 +0000)]
* merging some uf stuff from incremental_work branch that somehow nobody merged-in
* since two theories can propagate the same literal minisat now explicitly checks that a propagated literal has not been asserted yet

12 years agoadding additional checks for theories propagating literals that already have a value
Dejan Jovanović [Sat, 10 Dec 2011 08:34:41 +0000 (08:34 +0000)]
adding additional checks for theories propagating literals that already have a value

12 years agoa bit more changes, when propagting equalities/dis-equalities don't assert them to...
Dejan Jovanović [Sat, 10 Dec 2011 07:02:21 +0000 (07:02 +0000)]
a bit more changes, when propagting equalities/dis-equalities don't assert them to theories that rewrite them to true. for example, 1 != 0 rewrites to true, so it shouldn't get propagated to arithmetic.

12 years agoattempt to fix bug 293: if a split on a trivial shared pair is requested from a theor...
Dejan Jovanović [Sat, 10 Dec 2011 06:05:13 +0000 (06:05 +0000)]
attempt to fix bug 293: if a split on a trivial shared pair is requested from a theory, such as 1 = 0, it is reasserted to the theory.

12 years agoDisable a BV rewriter statistic (after checking with Liana) that was static,
Morgan Deters [Thu, 8 Dec 2011 19:23:45 +0000 (19:23 +0000)]
Disable a BV rewriter statistic (after checking with Liana) that was static,
and thus caused big problems with programs that create two SmtEngines in
one process.

If we need state like this in the rewriters, we'll need to make them
nonstatic.

12 years agoLemmaStatus changes, as agreed to during 12/2 meeting.
Morgan Deters [Tue, 6 Dec 2011 02:01:06 +0000 (02:01 +0000)]
LemmaStatus changes, as agreed to during 12/2 meeting.

12 years agooops, removing some integer operations that leaked in (they aren't part of trunk...
Morgan Deters [Tue, 6 Dec 2011 00:38:33 +0000 (00:38 +0000)]
oops, removing some integer operations that leaked in (they aren't part of trunk yet)

12 years agofix errors in smt-lib2 output; needed for debugging
Morgan Deters [Tue, 6 Dec 2011 00:34:32 +0000 (00:34 +0000)]
fix errors in smt-lib2 output; needed for debugging

12 years agochange short-circuiting behavior of Command execution in the main driver; allows...
Morgan Deters [Mon, 5 Dec 2011 21:11:19 +0000 (21:11 +0000)]
change short-circuiting behavior of Command execution in the main driver; allows a (limited) form of error recovery, matching what we had previously

12 years agoError detection is different now---with new Command infrastructure, exceptions are...
Morgan Deters [Fri, 2 Dec 2011 00:35:32 +0000 (00:35 +0000)]
Error detection is different now---with new Command infrastructure, exceptions are not thrown outside the library.  Reflect this in the exit code of the driver.  Fixes a bug found by Tim among the nightly regressions.

Also improved error reporting if antlr is unavailable and the parsers need to be generated.

12 years agodisable bug288.smt so that "make check" goes through---pending integers merge, see...
Morgan Deters [Wed, 30 Nov 2011 22:43:12 +0000 (22:43 +0000)]
disable bug288.smt so that "make check" goes through---pending integers merge, see bug #288

12 years agofix linking errors on oneiric
Morgan Deters [Wed, 30 Nov 2011 22:41:02 +0000 (22:41 +0000)]
fix linking errors on oneiric