cvc5.git
11 years agoMerge branch 'release-1.0.x'
François Bobot [Thu, 6 Dec 2012 12:28:53 +0000 (13:28 +0100)]
Merge branch 'release-1.0.x'

The commits have already been cherry-picked but this commit makes it clear.

11 years ago* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issues
Morgan Deters [Thu, 6 Dec 2012 01:38:17 +0000 (01:38 +0000)]
* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issues
* build bugfix for win32
* also fix a bug re: tuples and records in the datatypes rewriter

These fixes are for both trunk and 1.0.x branches.

(cherry picked from commit 8c8985f024cec925f774ff32ebccc306be8e4b26)

11 years agodistribute the find_public_interface.sh script
Morgan Deters [Mon, 3 Dec 2012 22:19:18 +0000 (22:19 +0000)]
distribute the find_public_interface.sh script
(cherry picked from commit af44cd27d5b079f1279c407e610e557e81285d8f)

11 years agoversion numbering
Morgan Deters [Mon, 3 Dec 2012 22:17:04 +0000 (22:17 +0000)]
version numbering
(cherry picked from commit 4cae70d893601a2070dc2b00c5640b48515b1a22)

11 years agoFix for fuzzer-found model bug
Clark Barrett [Mon, 3 Dec 2012 04:35:27 +0000 (04:35 +0000)]
Fix for fuzzer-found model bug

(cherry picked from commit 25c6e1331d338c6ba8d60224711343986e11cf79)

11 years ago* tuple and record support in compatibility library
Morgan Deters [Thu, 6 Dec 2012 01:54:11 +0000 (01:54 +0000)]
* tuple and record support in compatibility library

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years ago* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issues
Morgan Deters [Thu, 6 Dec 2012 01:38:17 +0000 (01:38 +0000)]
* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issues
* build bugfix for win32
* also fix a bug re: tuples and records in the datatypes rewriter

These fixes are for both trunk and 1.0.x branches.

11 years agoImproved garbage collection for TheoryArith. The merges all of the code over from...
Tim King [Wed, 5 Dec 2012 21:45:12 +0000 (21:45 +0000)]
Improved garbage collection for TheoryArith.  The merges all of the code over from branches/arithmetic/converge except for the new code for simplex.

11 years agoCleanup of arithmetic, and some new utility functions for the coming fcsimplex code.
Tim King [Wed, 5 Dec 2012 19:47:31 +0000 (19:47 +0000)]
Cleanup of arithmetic, and some new utility functions for the coming fcsimplex code.

11 years agoThis commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses CDInsert...
Tim King [Wed, 5 Dec 2012 19:06:21 +0000 (19:06 +0000)]
This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses CDInsertHashMap. CDHashSet<TNode> have been changed to CDHashSet<Node>.  Switching CnfStream to use CDInsertSet. Switches a few CDHashMaps in arithmetic to use CDTrailHashMap. Documentation changes to CDHashMap.

11 years ago* Add support for --decision=justification + incremental (bug 437)
Kshitij Bansal [Tue, 4 Dec 2012 21:41:51 +0000 (21:41 +0000)]
* Add support for --decision=justification + incremental (bug 437)
 - Fix a destruction order issue this triggered in DE

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agodistribute the find_public_interface.sh script
Morgan Deters [Mon, 3 Dec 2012 22:19:18 +0000 (22:19 +0000)]
distribute the find_public_interface.sh script

11 years agoversion numbering
Morgan Deters [Mon, 3 Dec 2012 22:17:04 +0000 (22:17 +0000)]
version numbering

11 years agoFix for fuzzer-found model bug
Clark Barrett [Mon, 3 Dec 2012 04:35:27 +0000 (04:35 +0000)]
Fix for fuzzer-found model bug

11 years agoCutting release 1.0.
Morgan Deters [Sat, 1 Dec 2012 18:51:31 +0000 (18:51 +0000)]
Cutting release 1.0.

11 years agofix cut-release sanity checks
Morgan Deters [Sat, 1 Dec 2012 17:58:02 +0000 (17:58 +0000)]
fix cut-release sanity checks

11 years agofix to TNode assertion (which is too strict, given lax ordering requirements on stati...
Morgan Deters [Sat, 1 Dec 2012 17:12:18 +0000 (17:12 +0000)]
fix to TNode assertion (which is too strict, given lax ordering requirements on static data initialization)---this should fix debug-staticbinary Mac builds, maybe others

11 years agoThrow a logic exception if user makes an assertion using a STORE_ALL
Clark Barrett [Sat, 1 Dec 2012 16:41:09 +0000 (16:41 +0000)]
Throw a logic exception if user makes an assertion using a STORE_ALL

11 years agoremove instantiator framework
Morgan Deters [Sat, 1 Dec 2012 15:13:58 +0000 (15:13 +0000)]
remove instantiator framework

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agoFix the way abstract values are typed; fixes some compliance issues.
Morgan Deters [Sat, 1 Dec 2012 14:36:14 +0000 (14:36 +0000)]
Fix the way abstract values are typed; fixes some compliance issues.

Also support array-store-all for Boolean terms (related to abstract values, since that's the only way for the user to include an array-store-all in an assertion).

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agofix memory corruption issue in debug builds that led to unhelpful output
Morgan Deters [Sat, 1 Dec 2012 13:47:50 +0000 (13:47 +0000)]
fix memory corruption issue in debug builds that led to unhelpful output

11 years agoremove an obsolete (and incorrect) assertion in boolean-terms; also add failing regre...
Morgan Deters [Sat, 1 Dec 2012 12:42:18 +0000 (12:42 +0000)]
remove an obsolete (and incorrect) assertion in boolean-terms; also add failing regression for bug 472

11 years agofix java system test dependences
Morgan Deters [Sat, 1 Dec 2012 12:18:57 +0000 (12:18 +0000)]
fix java system test dependences

11 years agodrastic simplification of quantifiers code regarding equality queries, instantiation...
Andrew Reynolds [Sat, 1 Dec 2012 02:57:59 +0000 (02:57 +0000)]
drastic simplification of quantifiers code regarding equality queries, instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine

11 years agoFix for a CLN related bug on 32 bit systems. Integer((1<<29)+1) and Integer((long...
Tim King [Sat, 1 Dec 2012 02:09:02 +0000 (02:09 +0000)]
Fix for a CLN related bug on 32 bit systems. Integer((1<<29)+1) and Integer((long int)((1<<29)+1)) gave different values.  This was confirmed on vm-int1.cims.nyu.edu. See ginac.de/CLN/cln_3.html#SEC15 for more details. rational_white and integer_white have tests covering this.

11 years agoSome fixes for boolean arrays
Morgan Deters [Sat, 1 Dec 2012 01:48:40 +0000 (01:48 +0000)]
Some fixes for boolean arrays

also a regression for bug 411

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agofix #line annotation warning
Morgan Deters [Sat, 1 Dec 2012 01:44:07 +0000 (01:44 +0000)]
fix #line annotation warning

11 years agoupdated examples
Morgan Deters [Sat, 1 Dec 2012 01:43:08 +0000 (01:43 +0000)]
updated examples

11 years agoadded a new example for the combination of bit-vectors and arrays (includes model...
Liana Hadarean [Sat, 1 Dec 2012 00:37:22 +0000 (00:37 +0000)]
added a new example for the combination of bit-vectors and arrays (includes model generation) and set the logic for the bitvector example

11 years agoanother part of last commit
Morgan Deters [Sat, 1 Dec 2012 00:33:50 +0000 (00:33 +0000)]
another part of last commit

11 years agodefinition-expansion fixed for get-model, resolves bug 411
Morgan Deters [Sat, 1 Dec 2012 00:31:38 +0000 (00:31 +0000)]
definition-expansion fixed for get-model, resolves bug 411

11 years agoPolishing API examples.
Tim King [Sat, 1 Dec 2012 00:11:20 +0000 (00:11 +0000)]
Polishing API examples.

11 years agoAdding SmtEngine::setLogic(const char* logic) so that smt.setLogic("QF_LRA"); works.
Tim King [Sat, 1 Dec 2012 00:08:38 +0000 (00:08 +0000)]
Adding SmtEngine::setLogic(const char* logic) so that smt.setLogic("QF_LRA"); works.

11 years agoFixes for stricter compilers Andy brought to my attention.
Tim King [Fri, 30 Nov 2012 23:34:47 +0000 (23:34 +0000)]
Fixes for stricter compilers Andy brought to my attention.

11 years agoChanging the documentation of ARR_TABLE_FUN to say (internal symbol).
Tim King [Fri, 30 Nov 2012 23:10:10 +0000 (23:10 +0000)]
Changing the documentation of ARR_TABLE_FUN to say (internal symbol).

11 years agoall API examples now have java versions too; bitvectors gets built; also updated...
Morgan Deters [Fri, 30 Nov 2012 23:07:19 +0000 (23:07 +0000)]
all API examples now have java versions too; bitvectors gets built; also updated old-style copyrights in the examples

11 years agoincorporating some comments from Clark
Morgan Deters [Fri, 30 Nov 2012 23:04:20 +0000 (23:04 +0000)]
incorporating some comments from Clark

11 years agoFix assertion in smt_engine's getValue
Clark Barrett [Fri, 30 Nov 2012 22:44:26 +0000 (22:44 +0000)]
Fix assertion in smt_engine's getValue
Minor changes to RELASE-NOTES

11 years agoUpdating the combination.cpp example.
Tim King [Fri, 30 Nov 2012 22:33:28 +0000 (22:33 +0000)]
Updating the combination.cpp example.

11 years agoCommitting tests to potentially discover an obscure CLN library issue on 32 bit platf...
Tim King [Fri, 30 Nov 2012 22:28:46 +0000 (22:28 +0000)]
Committing tests to potentially discover an obscure CLN library issue on 32 bit platforms. The issue is discussed here: ginac.de/CLN/cln_3.html#SEC15.

11 years agorenaming --smtlib to --smtlib-strict; removing --smtlib2 option
Morgan Deters [Fri, 30 Nov 2012 22:28:06 +0000 (22:28 +0000)]
renaming --smtlib to --smtlib-strict; removing --smtlib2 option

11 years agointernal variables (skolems) aren't printed as part of the model
Morgan Deters [Fri, 30 Nov 2012 21:43:11 +0000 (21:43 +0000)]
internal variables (skolems) aren't printed as part of the model

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agochange detection/handling of output language more reasonably; fixes a nagging bug...
Morgan Deters [Fri, 30 Nov 2012 21:31:12 +0000 (21:31 +0000)]
change detection/handling of output language more reasonably; fixes a nagging bug Tim found in API examples

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agoquantifiers now uses master equality engine, preparation work to cleanup code
Andrew Reynolds [Fri, 30 Nov 2012 20:38:45 +0000 (20:38 +0000)]
quantifiers now uses master equality engine, preparation work to cleanup code

11 years agoparametric datatypes fix related to non-ascribed type constructors introduced by...
Andrew Reynolds [Fri, 30 Nov 2012 20:21:39 +0000 (20:21 +0000)]
parametric datatypes fix related to non-ascribed type constructors introduced by decision procedure

11 years agoadded a simple API example example showing how to use the bit-vector theory.
Liana Hadarean [Fri, 30 Nov 2012 19:44:52 +0000 (19:44 +0000)]
added a simple API example example showing how to use the bit-vector theory.

11 years agoChanges to SExpr to accept autoconversion from bool and const char*. Adding an exampl...
Tim King [Fri, 30 Nov 2012 18:30:37 +0000 (18:30 +0000)]
Changes to SExpr to accept autoconversion from bool and const char*. Adding an example for combination.

11 years agoAdding smtname level options for tlimit, rlimit, etc. Fix to the internal documentati...
Tim King [Fri, 30 Nov 2012 18:16:59 +0000 (18:16 +0000)]
Adding smtname level options for tlimit, rlimit, etc. Fix to the internal documentation in base_options.

11 years agoPartial fix for bug 435; still needs some effort.
Morgan Deters [Fri, 30 Nov 2012 18:11:48 +0000 (18:11 +0000)]
Partial fix for bug 435; still needs some effort.

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agoAdd some regressions for bug 438.
Morgan Deters [Fri, 30 Nov 2012 15:29:36 +0000 (15:29 +0000)]
Add some regressions for bug 438.

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agofix rewrite-rules syntax in regression
Morgan Deters [Fri, 30 Nov 2012 15:14:36 +0000 (15:14 +0000)]
fix rewrite-rules syntax in regression

11 years agominor fix to release script
Morgan Deters [Fri, 30 Nov 2012 14:07:11 +0000 (14:07 +0000)]
minor fix to release script

11 years agofix the syntax of assert-rewrite/-propagation/-reduction by putting the pattern first
François Bobot [Fri, 30 Nov 2012 11:35:02 +0000 (11:35 +0000)]
fix the syntax of assert-rewrite/-propagation/-reduction by putting the pattern first
just after the bindings

 Do it before the release in order to not break user files later

11 years agoreliable benchmark corresponding to bug468
Kshitij Bansal [Thu, 29 Nov 2012 23:55:37 +0000 (23:55 +0000)]
reliable benchmark corresponding to bug468

11 years agorequire type ascriptions for parametric datatype constructors (making them canonical...
Andrew Reynolds [Thu, 29 Nov 2012 23:28:29 +0000 (23:28 +0000)]
require type ascriptions for parametric datatype constructors (making them canonical), this fixes the followup issue of bug 438

11 years agoFix for hidden symbols in library on Mac. It's a strange issue to do with
Morgan Deters [Thu, 29 Nov 2012 23:08:25 +0000 (23:08 +0000)]
Fix for hidden symbols in library on Mac.  It's a strange issue to do with
explicit template instantiation rules, -fvisibility=hidden, and the way that
Apple distributes libstdc++.

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agofixes bug 438, incorporate subtypes into type unification when typechecking parameter...
Andrew Reynolds [Thu, 29 Nov 2012 22:02:20 +0000 (22:02 +0000)]
fixes bug 438, incorporate subtypes into type unification when typechecking parameterized datatypes

11 years agofix for andy: boolean terms stuff really shouldn't look at datatypes at all in this...
Morgan Deters [Thu, 29 Nov 2012 21:34:16 +0000 (21:34 +0000)]
fix for andy: boolean terms stuff really shouldn't look at datatypes at all in this release

11 years agominor documentation fix
Morgan Deters [Thu, 29 Nov 2012 19:37:32 +0000 (19:37 +0000)]
minor documentation fix

11 years agosvn:ignore property
Morgan Deters [Thu, 29 Nov 2012 18:15:56 +0000 (18:15 +0000)]
svn:ignore property

11 years agoFix for nasty corner case found by fuzzer...
Clark Barrett [Thu, 29 Nov 2012 14:28:28 +0000 (14:28 +0000)]
Fix for nasty corner case found by fuzzer...

11 years agoHack to support global variables for CVC language extended to export mechanism.
Kshitij Bansal [Thu, 29 Nov 2012 06:59:21 +0000 (06:59 +0000)]
Hack to support global variables for CVC language extended to export mechanism.
- Adds GlobalVarAttr node attribute

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agoFixing function models with Boolean terms. Also, LAMBDA's should not be const.
Clark Barrett [Thu, 29 Nov 2012 00:59:06 +0000 (00:59 +0000)]
Fixing function models with Boolean terms.  Also, LAMBDA's should not be const.

11 years agoAdding the helloworld.cpp example.
Tim King [Wed, 28 Nov 2012 22:59:58 +0000 (22:59 +0000)]
Adding the helloworld.cpp example.

11 years agofix a potential race (have failed to reproduce)
Kshitij Bansal [Wed, 28 Nov 2012 21:52:56 +0000 (21:52 +0000)]
fix a potential race (have failed to reproduce)

11 years agoFix for getValue. Now it can handle lambda applications
Clark Barrett [Wed, 28 Nov 2012 21:26:43 +0000 (21:26 +0000)]
Fix for getValue.  Now it can handle lambda applications

11 years agoAttempted "quick-fix" for QF_UF performance regression since Boolean terms added.
Morgan Deters [Wed, 28 Nov 2012 21:18:05 +0000 (21:18 +0000)]
Attempted "quick-fix" for QF_UF performance regression since Boolean terms added.

Sharing is turned on only when Boolean terms are detected during preprocessing.  QF_UF problems (and others)
that don't use any Boolean terms won't have BV turned on.

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agotreat all get commands like getValue (send only to lastWinner)
Kshitij Bansal [Wed, 28 Nov 2012 20:18:46 +0000 (20:18 +0000)]
treat all get commands like getValue (send only to lastWinner)

11 years agominor
Kshitij Bansal [Wed, 28 Nov 2012 18:37:51 +0000 (18:37 +0000)]
minor

11 years agoupdate to release notes
Morgan Deters [Wed, 28 Nov 2012 18:00:10 +0000 (18:00 +0000)]
update to release notes

11 years agoBug fix:
Morgan Deters [Wed, 28 Nov 2012 17:37:57 +0000 (17:37 +0000)]
Bug fix:
* Fix creation of bound variables in CVC native language parser
* This corrects a problem with misleading model output

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agofix: correct misleading comment in dump output
Morgan Deters [Wed, 28 Nov 2012 17:23:37 +0000 (17:23 +0000)]
fix: correct misleading comment in dump output

11 years agoFunctions and predicates over Boolean now work with --check-models and output correct
Morgan Deters [Tue, 27 Nov 2012 22:40:05 +0000 (22:40 +0000)]
Functions and predicates over Boolean now work with --check-models and output correct
models for such functions (though they are somewhat ugly at present).

There's still a problem with model extraction, but it's not Boolean terms' fault.
Sometimes checkModel() can report that the model is just fine, but if a user extracts
values with getValue(), they find problems with the model (i.e., it doesn't satisfy some
assertions).  This appears to be due to an asymmetry between how checkModel() works and
how Model::getValue() works.  I'll open a bugzilla report to discuss this after thinking
some more on it.

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agofix in CommandSequence invoke : maintain success/failure. Fixes bug 465.
Kshitij Bansal [Tue, 27 Nov 2012 21:31:46 +0000 (21:31 +0000)]
fix in CommandSequence invoke : maintain success/failure. Fixes bug 465.

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agomore mac fixes
Morgan Deters [Tue, 27 Nov 2012 19:18:12 +0000 (19:18 +0000)]
more mac fixes

11 years agofix for some Mac builds
Morgan Deters [Tue, 27 Nov 2012 19:05:13 +0000 (19:05 +0000)]
fix for some Mac builds

11 years agoSimplify --help=decision with only currently supported options
Kshitij Bansal [Tue, 27 Nov 2012 19:02:50 +0000 (19:02 +0000)]
Simplify --help=decision with only currently supported options

Add notice/warning when using incremental-mode + decision (it was
already disabled)

Some other minor cleanup

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agogive warning at configure-time about unsupported language bindings, and don't adverti...
Morgan Deters [Tue, 27 Nov 2012 18:09:16 +0000 (18:09 +0000)]
give warning at configure-time about unsupported language bindings, and don't advertise them in help listing for --enable-language-bindings

11 years agodo not turn on BV for QF_SAT
Morgan Deters [Tue, 27 Nov 2012 17:52:01 +0000 (17:52 +0000)]
do not turn on BV for QF_SAT

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agoFirst chunk of boolean-terms support.
Morgan Deters [Tue, 27 Nov 2012 05:52:21 +0000 (05:52 +0000)]
First chunk of boolean-terms support.

Passes simple tests and doesn't break existing functionality.
Still need some work merged in for models.

This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV).  Tonight's nightly regression run should tell us if/how that hurts performance.

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agoTuples and records merge. Resolves bug 270.
Morgan Deters [Tue, 27 Nov 2012 02:13:38 +0000 (02:13 +0000)]
Tuples and records merge.  Resolves bug 270.

Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together.

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agoAdding an example to show how to use arithmetic.
Tim King [Tue, 27 Nov 2012 01:39:58 +0000 (01:39 +0000)]
Adding an example to show how to use arithmetic.

11 years agoImproved implementation of Integer::length() with CLN enabled. Additional tests...
Tim King [Mon, 26 Nov 2012 21:38:28 +0000 (21:38 +0000)]
Improved implementation of Integer::length() with CLN enabled.  Additional tests to sanity check both versions CLN and GMP versions of length.

11 years agoinclude new regression directories in summary test output
Morgan Deters [Mon, 26 Nov 2012 20:05:02 +0000 (20:05 +0000)]
include new regression directories in summary test output

11 years agorolling back r4625 for now (closes bug 464), Andy we should talk about this a bit...
Morgan Deters [Mon, 26 Nov 2012 19:39:03 +0000 (19:39 +0000)]
rolling back r4625 for now (closes bug 464), Andy we should talk about this a bit more..

11 years agofixup for incremental solving
Dejan Jovanović [Mon, 26 Nov 2012 17:40:31 +0000 (17:40 +0000)]
fixup for incremental solving

11 years agoRemoving DioSolver::acceptableOriginalNodes(). This assertion was too strong, and...
Tim King [Mon, 26 Nov 2012 17:30:44 +0000 (17:30 +0000)]
Removing DioSolver::acceptableOriginalNodes(). This assertion was too strong, and was broken by r4620. This commit resolves bug463. Adding a previously triggering test case.

11 years agoAdding support for a master equality engine. Each theory gets the master equality...
Dejan Jovanović [Mon, 26 Nov 2012 17:07:46 +0000 (17:07 +0000)]
Adding support for a master equality engine. Each theory gets the master equality engine through the setMasterEqualityEngine method. This is a read-only equality engine, so nothing should be added to it directly. Instead each equality engine that is of interest should have the master equality engine attached to it. To set when to use the master equality engine see TheoryEngine::finishInit().

11 years agoImproving arithmetic debugging output.
Tim King [Mon, 26 Nov 2012 17:02:34 +0000 (17:02 +0000)]
Improving arithmetic debugging output.

11 years agoDisabling test/regress/regress0/push-pop/bug396.smt2. This takes 2m to run in debug...
Tim King [Mon, 26 Nov 2012 17:01:48 +0000 (17:01 +0000)]
Disabling test/regress/regress0/push-pop/bug396.smt2. This takes 2m to run in debug mode. This is too long for a regress0 test.

11 years agodon't include internal variables in model output
Morgan Deters [Mon, 26 Nov 2012 15:00:26 +0000 (15:00 +0000)]
don't include internal variables in model output

11 years agosome fixes to language bindings and function visibility
Morgan Deters [Mon, 26 Nov 2012 14:39:56 +0000 (14:39 +0000)]
some fixes to language bindings and function visibility

11 years agoMakefile fix for new versions of Make (thanks Clark for noticing this); see e.g....
Morgan Deters [Mon, 26 Nov 2012 13:42:27 +0000 (13:42 +0000)]
Makefile fix for new versions of Make (thanks Clark for noticing this); see e.g. osdir.com/ml/bug-make-gnu/2011-04/msg00011.html

12 years agoAdding a regression test from bug 462.
Tim King [Sun, 25 Nov 2012 01:02:49 +0000 (01:02 +0000)]
Adding a regression test from bug 462.

12 years agoThis commit fixes two incompleteness bugs (461, 459) introduced in r4611 dues to...
Tim King [Sun, 25 Nov 2012 00:49:25 +0000 (00:49 +0000)]
This commit fixes two incompleteness bugs (461, 459) introduced in r4611 dues to a problem of not correctly handling disequalities.  Performance implications are uncertain.

12 years agoAdds ensureConstraint(...) to ConstraintDatabase. This is a slightly optimized way...
Tim King [Sat, 24 Nov 2012 23:32:04 +0000 (23:32 +0000)]
Adds ensureConstraint(...) to ConstraintDatabase. This is a slightly optimized way of doing getConstraint() if the user already has a ValueCollection&.

12 years agoExample of rewrite rules use that comes from an harness test
François Bobot [Fri, 23 Nov 2012 14:37:40 +0000 (14:37 +0000)]
Example of rewrite rules use that comes from an harness test

12 years ago- Removes getDeltaValueWithNonlinear() entirely
Tim King [Wed, 21 Nov 2012 18:46:23 +0000 (18:46 +0000)]
- Removes getDeltaValueWithNonlinear() entirely
- Changes the signature of getDeltaValue to throw DeltaRationalException and ModelException
-- DeltaRationalExceptions can occur with non-linear arithmetic computations that cannot be done. (0 + delta) * (1 + delta) is not a DeltaRational.
-- ModelExceptions occur if getDeltaValue() is going to return a value that disagrees with its value in the model (due to non-linear arithmetic)
-- ModelExceptions also occur if getDeltaValue(n) is called on a variable arithmetic has never seen before.
- getEqualityStatus() now wraps and catches both of these exceptions. If either occurs, the equality status is EQUALITY_UNKNOWN. This allows arithmetic to handle terms it has never seen before in getEqualityStatus. This resolves bug 453.
- Removes the dead code rowImplication() entirely.

12 years agoAdds a number of new capabilities to DeltaRational. This adds DeltaRationalException...
Tim King [Wed, 21 Nov 2012 18:36:29 +0000 (18:36 +0000)]
Adds a number of new capabilities to DeltaRational. This adds DeltaRationalException which can be called when an operation on a DeltaRational does not have well formed semantics. This allows for things like multiplying two DeltaRationals, which may or may not result in a DeltaRational.

12 years agoAdded debugging output to --check-models. I've found this output quite useful while...
Tim King [Wed, 21 Nov 2012 18:31:55 +0000 (18:31 +0000)]
Added debugging output to --check-models. I've found this output quite useful while debugging.