cvc5.git
11 years agoSome final minor changes before cutting 1.1.
Morgan Deters [Wed, 3 Apr 2013 17:08:00 +0000 (13:08 -0400)]
Some final minor changes before cutting 1.1.

* update documentation
* update the cut-release script
* spelling/wording updates
* add a (previously-failing) fuzzer regression

11 years agoupdated NEWS to include inequality solver
Liana Hadarean [Wed, 3 Apr 2013 16:53:15 +0000 (12:53 -0400)]
updated NEWS to include inequality solver

11 years agoabort quantifiers check if master equality engine is inconsistent.
Andrew Reynolds [Wed, 3 Apr 2013 07:09:17 +0000 (02:09 -0500)]
abort quantifiers check if master equality engine is inconsistent.

11 years agoMaking arithmetic model reversion on unsat checks an option.
Tim King [Tue, 2 Apr 2013 18:51:06 +0000 (14:51 -0400)]
Making arithmetic model reversion on unsat checks an option.

11 years agoRegenerated copyrights: canonicalized names, no emails
Morgan Deters [Tue, 2 Apr 2013 18:31:53 +0000 (14:31 -0400)]
Regenerated copyrights: canonicalized names, no emails

11 years agoRemove old README file from rewrite-rules left over from new-theory script long ago
Morgan Deters [Tue, 2 Apr 2013 17:59:58 +0000 (13:59 -0400)]
Remove old README file from rewrite-rules left over from new-theory script long ago

11 years agoFix get-authors script to not extract email addresses, canonicalize names, add .mailmap
Morgan Deters [Tue, 2 Apr 2013 17:34:55 +0000 (13:34 -0400)]
Fix get-authors script to not extract email addresses, canonicalize names, add .mailmap

11 years agoOne final fix to "make submission" rule
Morgan Deters [Tue, 2 Apr 2013 14:44:24 +0000 (10:44 -0400)]
One final fix to "make submission" rule

11 years agoupdate copyrights
Morgan Deters [Tue, 2 Apr 2013 03:32:39 +0000 (23:32 -0400)]
update copyrights

11 years agoAdjust release Makefile rules, new run script
Morgan Deters [Tue, 2 Apr 2013 03:26:46 +0000 (23:26 -0400)]
Adjust release Makefile rules, new run script

11 years agoFix regression error by turning off model-based solver when models are on
Clark Barrett [Tue, 2 Apr 2013 03:06:13 +0000 (23:06 -0400)]
Fix regression error by turning off model-based solver when models are on
(ironic, yes, but model-based solver doesn't yet produce models)

11 years agoTurning on model based array solver for QF_AX
Clark Barrett [Tue, 2 Apr 2013 02:38:52 +0000 (22:38 -0400)]
Turning on model based array solver for QF_AX

11 years agoMade eager lemmas an option, enabled for QF_AX
Clark Barrett [Tue, 2 Apr 2013 02:27:17 +0000 (22:27 -0400)]
Made eager lemmas an option, enabled for QF_AX

11 years agoDisabling eager array index splitting for QF_AX
Clark Barrett [Tue, 2 Apr 2013 00:06:09 +0000 (20:06 -0400)]
Disabling eager array index splitting for QF_AX

11 years agoFixes for two bugs:
Morgan Deters [Mon, 1 Apr 2013 21:34:27 +0000 (17:34 -0400)]
Fixes for two bugs:

* one that Tim found in model generation for records containing Booleans
* another that the fuzzer found in quantifiers + check-models

Test cases enabled/added for both.

11 years agoCleaning up the demand restart code.
Tim King [Mon, 1 Apr 2013 23:42:43 +0000 (19:42 -0400)]
Cleaning up the demand restart code.

11 years agoAdding a restart test strategy to integers.
Tim King [Mon, 1 Apr 2013 15:26:57 +0000 (11:26 -0400)]
Adding a restart test strategy to integers.

11 years agoAdding demand restart.
Tim King [Mon, 1 Apr 2013 15:26:14 +0000 (11:26 -0400)]
Adding demand restart.

11 years agoAdding tests for the previous commit.
Tim King [Mon, 1 Apr 2013 21:26:13 +0000 (17:26 -0400)]
Adding tests for the previous commit.

11 years agoMerging some cleanup work:
Morgan Deters [Wed, 20 Mar 2013 22:16:26 +0000 (18:16 -0400)]
Merging some cleanup work:

* Comment cleanup
* Spelling fixes
* Fix warnings
* Documentation updates
* References in docs to cryptominisat removed
* Unneeded scope resolutions removed
* Old, unused regression removed

11 years agoFix for iff terms over equalities between the same term and differing constants.
Tim King [Mon, 1 Apr 2013 19:39:25 +0000 (15:39 -0400)]
Fix for iff terms over equalities between the same term and differing constants.

11 years agoFix bug 491 and related issues with checkModel() and quantifiers. Enabling previousl...
Morgan Deters [Thu, 7 Feb 2013 23:13:01 +0000 (18:13 -0500)]
Fix bug 491 and related issues with checkModel() and quantifiers.  Enabling previously-failing testcase.

11 years agofixed TheoryBool rewriter bug
lianah [Mon, 1 Apr 2013 19:23:46 +0000 (15:23 -0400)]
fixed TheoryBool rewriter bug

11 years agofixed bug 502; now the core bv solver only gives the model for variables and shared...
lianah [Mon, 1 Apr 2013 18:04:58 +0000 (14:04 -0400)]
fixed bug 502; now the core bv solver only gives the model for variables and shared terms.

11 years agochanged option to run inequality solver by default
Liana Hadarean [Sun, 31 Mar 2013 03:47:03 +0000 (23:47 -0400)]
changed option to run inequality solver by default

11 years agoDisabling eager array index splitting for QF_AUFLIA
Clark Barrett [Sun, 31 Mar 2013 00:27:37 +0000 (20:27 -0400)]
Disabling eager array index splitting for QF_AUFLIA
Minor changes to model-based array solver

11 years agodo simple ite rewriting within quantifiers
Andrew Reynolds [Sat, 30 Mar 2013 22:29:34 +0000 (17:29 -0500)]
do simple ite rewriting within quantifiers

11 years agomake Boolean term conversion partially non-recursive (resolves bug 501)
Morgan Deters [Fri, 29 Mar 2013 20:50:13 +0000 (16:50 -0400)]
make Boolean term conversion partially non-recursive (resolves bug 501)

11 years agoMerge branch 'master' of github.com:CVC4/CVC4
Dejan Jovanović [Fri, 29 Mar 2013 14:57:50 +0000 (10:57 -0400)]
Merge branch 'master' of github.com:CVC4/CVC4

11 years agoremoving cryptominisat since we're not using it
Dejan Jovanović [Fri, 29 Mar 2013 14:57:22 +0000 (10:57 -0400)]
removing cryptominisat since we're not using it

11 years agofix memory corruption in arrays destructor
Morgan Deters [Thu, 28 Mar 2013 16:37:37 +0000 (12:37 -0400)]
fix memory corruption in arrays destructor

11 years agosome Java bindings fixes (fixes Debian build problems)
Morgan Deters [Thu, 28 Mar 2013 03:42:13 +0000 (23:42 -0400)]
some Java bindings fixes (fixes Debian build problems)

11 years agoFixed a warning, made eager-index default to true (better for QF_AUFBV)
Clark Barrett [Thu, 28 Mar 2013 03:02:29 +0000 (23:02 -0400)]
Fixed a warning, made eager-index default to true (better for QF_AUFBV)

11 years agoFixed bug in arrays
Clark Barrett [Thu, 28 Mar 2013 02:43:18 +0000 (22:43 -0400)]
Fixed bug in arrays

11 years agoAdded assertion
Clark Barrett [Thu, 28 Mar 2013 00:34:18 +0000 (20:34 -0400)]
Added assertion

11 years agoUpdates to model-based array solver
Clark Barrett [Wed, 27 Mar 2013 20:38:41 +0000 (16:38 -0400)]
Updates to model-based array solver
Minor fixes to bv and theory_engine

11 years agoNew model-based array procedure
Clark Barrett [Wed, 27 Mar 2013 00:12:47 +0000 (20:12 -0400)]
New model-based array procedure

11 years agoreverted the core solver to do static slicing, added option --bv-core-solver
lianah [Wed, 27 Mar 2013 21:48:39 +0000 (17:48 -0400)]
reverted the core solver to do static slicing, added option --bv-core-solver

11 years agofixed inequality checkDisequalities inefficiency
lianah [Wed, 27 Mar 2013 19:10:57 +0000 (15:10 -0400)]
fixed inequality checkDisequalities inefficiency

11 years agoMerge branch 'master' into bv-core
lianah [Wed, 27 Mar 2013 18:07:59 +0000 (14:07 -0400)]
Merge branch 'master' into bv-core

11 years agofixed some model stuff
lianah [Wed, 27 Mar 2013 18:05:49 +0000 (14:05 -0400)]
fixed some model stuff

11 years agofixed model generation bug; commented out attempt at inequality propagation
lianah [Wed, 27 Mar 2013 04:29:18 +0000 (00:29 -0400)]
fixed  model generation bug; commented out attempt at inequality propagation

11 years agoinequality solver now only splits on disequalities when complete
lianah [Wed, 27 Mar 2013 03:34:25 +0000 (23:34 -0400)]
inequality solver now only splits on disequalities when complete

11 years agoadded model generation for bv subtheories and bv-inequality solver option
lianah [Wed, 27 Mar 2013 02:14:24 +0000 (22:14 -0400)]
added model generation for bv subtheories and bv-inequality solver option

11 years agoFixes for warnings from clang++, from -std=gnu++0x, from swig, and from javac
Morgan Deters [Tue, 26 Mar 2013 21:58:39 +0000 (17:58 -0400)]
Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javac

11 years agoMake --incremental the default when running interactively
Morgan Deters [Tue, 26 Mar 2013 21:58:33 +0000 (17:58 -0400)]
Make --incremental the default when running interactively

11 years agocore theory currently disabled
lianah [Tue, 26 Mar 2013 20:55:29 +0000 (16:55 -0400)]
core theory currently disabled

11 years agogetModelValue implementation in bitvectors
Dejan Jovanović [Tue, 26 Mar 2013 20:52:21 +0000 (16:52 -0400)]
getModelValue implementation in bitvectors

11 years agoadding
Dejan Jovanović [Tue, 26 Mar 2013 20:47:47 +0000 (16:47 -0400)]
adding
* getModelValue to valuation
* getModelValue to theory engine
* getModelValue to theory
implemented getModelValue in bitvector

the purpose of getModelValue is to ask for a concrete value of a shared term

11 years agoMerge branch 'master' of git@github.com:CVC4/CVC4.git
Dejan Jovanović [Tue, 26 Mar 2013 20:17:40 +0000 (16:17 -0400)]
Merge branch 'master' of git@github.com:CVC4/CVC4.git

11 years agomoving bv before arrays
Dejan Jovanović [Tue, 26 Mar 2013 20:17:27 +0000 (16:17 -0400)]
moving bv before arrays

11 years agofixed inequality bugs due to improper explanation
lianah [Tue, 26 Mar 2013 19:36:47 +0000 (15:36 -0400)]
fixed inequality bugs due to improper explanation

11 years agocleaned up the bv subtheory interface; added check for inequality theory completeness
lianah [Tue, 26 Mar 2013 00:37:31 +0000 (20:37 -0400)]
cleaned up the bv subtheory interface; added check for inequality theory completeness

11 years agojava input stream adapters working
Morgan Deters [Fri, 1 Mar 2013 23:31:10 +0000 (18:31 -0500)]
java input stream adapters working

11 years agogetEqualityStatus now also queries the inequality solver
lianah [Mon, 25 Mar 2013 22:24:29 +0000 (18:24 -0400)]
getEqualityStatus now also queries the inequality solver

11 years agoFix for SCM detection
Morgan Deters [Mon, 25 Mar 2013 22:14:37 +0000 (18:14 -0400)]
Fix for SCM detection

11 years agoMerge pull request #7 from kbansal/portfolio
Kshitij Bansal [Mon, 25 Mar 2013 21:16:31 +0000 (14:16 -0700)]
Merge pull request #7 from kbansal/portfolio

finish removal of separateOutput

11 years agofinish removal of separateOutput
Kshitij Bansal [Mon, 25 Mar 2013 21:15:11 +0000 (17:15 -0400)]
finish removal of separateOutput

11 years agoadded support for disequalities in the inequality solver
Liana Hadarean [Mon, 25 Mar 2013 03:38:33 +0000 (23:38 -0400)]
added support for disequalities in the inequality solver

11 years agoincremental inequality solver implemented
lianah [Sun, 24 Mar 2013 22:50:39 +0000 (18:50 -0400)]
incremental inequality solver implemented

11 years agoFix bug in portfolio executor output; fixes nightly portfolio-checking runs.
Morgan Deters [Sun, 24 Mar 2013 01:38:55 +0000 (21:38 -0400)]
Fix bug in portfolio executor output; fixes nightly portfolio-checking runs.

11 years agonon-incremental inequality solver seems to be bug-free (i.e. passes fuzzing)
lianah [Sat, 23 Mar 2013 21:19:21 +0000 (17:19 -0400)]
non-incremental inequality solver seems to be bug-free (i.e. passes fuzzing)

11 years agofixed some explanation problems for the core theory; still slow
lianah [Sat, 23 Mar 2013 17:40:29 +0000 (13:40 -0400)]
fixed some explanation problems for the core theory; still slow

11 years agoMerge remote-tracking branch 'dddejan/c++11'
Dejan Jovanović [Sat, 23 Mar 2013 05:19:06 +0000 (01:19 -0400)]
Merge remote-tracking branch 'dddejan/c++11'

Conflicts:
src/smt/boolean_terms.cpp

11 years agochanging string hash function to use the gnu namespace
Dejan Jovanović [Sat, 23 Mar 2013 04:27:42 +0000 (00:27 -0400)]
changing string hash function to use the gnu namespace
due to namesapce resolution std namespace was used instead, which hashes the string pointers leading to mayhem

11 years agoSupport for Boolean term conversion in datatypes.
Morgan Deters [Mon, 28 Jan 2013 22:31:57 +0000 (17:31 -0500)]
Support for Boolean term conversion in datatypes.

11 years agocompiles with
Dejan Jovanović [Fri, 22 Mar 2013 21:25:48 +0000 (17:25 -0400)]
compiles with
export CXXFLAGS='-std=gnu++0x' before configure
fails all regressions in the parser

11 years agoMerge branch 'master' into bv-core
lianah [Fri, 22 Mar 2013 00:43:29 +0000 (20:43 -0400)]
Merge branch 'master' into bv-core

11 years agoanother typo/bugfix for equality constant evaluation
Dejan Jovanović [Fri, 22 Mar 2013 00:07:44 +0000 (20:07 -0400)]
another typo/bugfix for equality constant evaluation

11 years agoMerge branch 'master' into bv-core
lianah [Thu, 21 Mar 2013 23:26:49 +0000 (19:26 -0400)]
Merge branch 'master' into bv-core

11 years agofixed more equality stuff
lianah [Thu, 21 Mar 2013 23:25:33 +0000 (19:25 -0400)]
fixed more equality stuff

11 years agoBetter error in case of nonlinear assertions while in linear logic
Morgan Deters [Wed, 13 Mar 2013 22:27:11 +0000 (18:27 -0400)]
Better error in case of nonlinear assertions while in linear logic

11 years agoAdd the ability to "mute" commands, needed for SMT-LIB compliance.
Morgan Deters [Thu, 21 Mar 2013 18:30:32 +0000 (14:30 -0400)]
Add the ability to "mute" commands, needed for SMT-LIB compliance.

11 years agofixing markings of internal nodes in equality engine
Dejan Jovanović [Thu, 21 Mar 2013 20:20:06 +0000 (16:20 -0400)]
fixing markings of internal nodes in equality engine

11 years agofixed compilation problem
lianah [Thu, 21 Mar 2013 19:46:52 +0000 (15:46 -0400)]
fixed compilation problem

11 years agoincorporated dejan's constant evaluation; now getting destruction seg fault
lianah [Thu, 21 Mar 2013 19:43:58 +0000 (15:43 -0400)]
incorporated dejan's constant evaluation; now getting destruction seg fault

11 years agoMerge branch 'master' into bv-core
lianah [Thu, 21 Mar 2013 18:33:45 +0000 (14:33 -0400)]
Merge branch 'master' into bv-core

11 years agodisabled ineq
lianah [Thu, 21 Mar 2013 18:30:48 +0000 (14:30 -0400)]
disabled ineq

11 years agoMerge branch 'master' of github.com:CVC4/CVC4
Dejan Jovanović [Thu, 21 Mar 2013 18:28:46 +0000 (14:28 -0400)]
Merge branch 'master' of github.com:CVC4/CVC4

11 years agoSome model and printing fixes for defined functions in input.
Morgan Deters [Thu, 21 Mar 2013 18:04:35 +0000 (14:04 -0400)]
Some model and printing fixes for defined functions in input.

11 years agomore equality constant evaluation
Dejan Jovanović [Thu, 21 Mar 2013 18:26:54 +0000 (14:26 -0400)]
more equality constant evaluation

11 years agoFix for SmtEngine::expandDefinitions()---improper TypeCheckingException
Morgan Deters [Wed, 20 Feb 2013 23:11:54 +0000 (18:11 -0500)]
Fix for SmtEngine::expandDefinitions()---improper TypeCheckingException

11 years agoadded regression test for constant eval
lianah [Thu, 21 Mar 2013 16:38:51 +0000 (12:38 -0400)]
added regression test for constant eval

11 years agoMerge branch 'master' into bv-core
lianah [Thu, 21 Mar 2013 15:41:39 +0000 (11:41 -0400)]
Merge branch 'master' into bv-core

11 years agofixing constant evaluation bugs
Dejan Jovanović [Thu, 21 Mar 2013 04:21:24 +0000 (00:21 -0400)]
fixing constant evaluation bugs

11 years agoadded more tests
lianah [Thu, 21 Mar 2013 02:33:39 +0000 (22:33 -0400)]
added more tests

11 years agogeneralized bv inequality reasoning to handle both strict and non-strict inequalities
lianah [Thu, 21 Mar 2013 01:10:10 +0000 (21:10 -0400)]
generalized bv inequality reasoning to handle both strict and non-strict inequalities

11 years agoBetter reporting of detached git state in --version and --show-config
Morgan Deters [Wed, 20 Mar 2013 22:46:45 +0000 (18:46 -0400)]
Better reporting of detached git state in --version and --show-config

11 years agoFix to bug 497: make justification heuristic's ITE cache context-dependent.
Morgan Deters [Tue, 12 Mar 2013 23:41:28 +0000 (19:41 -0400)]
Fix to bug 497: make justification heuristic's ITE cache context-dependent.

11 years agoRemove unintentionally-committed-to-master README from interactive branch
Morgan Deters [Thu, 21 Mar 2013 00:00:40 +0000 (20:00 -0400)]
Remove unintentionally-committed-to-master README from interactive branch

11 years agoInteractive mode support for multiline input
Morgan Deters [Wed, 12 Dec 2012 22:28:14 +0000 (17:28 -0500)]
Interactive mode support for multiline input

11 years agoProperly |quote| symbols in SMT-LIBv2 output.
Morgan Deters [Wed, 20 Mar 2013 17:09:18 +0000 (13:09 -0400)]
Properly |quote| symbols in SMT-LIBv2 output.

11 years agoSome statistics for narrowing down incrementality issues (push/pop vs solve timing)
Morgan Deters [Tue, 5 Mar 2013 23:52:20 +0000 (18:52 -0500)]
Some statistics for narrowing down incrementality issues (push/pop vs solve timing)

11 years agoone more ineq regression
Liana Hadarean [Wed, 20 Mar 2013 04:59:15 +0000 (00:59 -0400)]
one more ineq regression

11 years agofixed reversed concat in core theory
Liana Hadarean [Wed, 20 Mar 2013 03:39:25 +0000 (23:39 -0400)]
fixed reversed concat in core theory

11 years agomerged dejan's stuff
Liana Hadarean [Wed, 20 Mar 2013 02:25:40 +0000 (22:25 -0400)]
merged dejan's stuff

11 years agomerged master with dejan's constant evaluating equality engine
Liana Hadarean [Wed, 20 Mar 2013 02:09:55 +0000 (22:09 -0400)]
merged master with dejan's constant evaluating equality engine

11 years agoinequality reasoning works on small examples added to regressions (not incremental...
Liana Hadarean [Wed, 20 Mar 2013 01:54:22 +0000 (21:54 -0400)]
inequality reasoning works on small examples added to regressions (not incremental); currently disabled though

11 years agoAdding evaluation of constant terms to the equality engine. Evaluation on a particula...
Dejan Jovanović [Wed, 20 Mar 2013 01:10:27 +0000 (21:10 -0400)]
Adding evaluation of constant terms to the equality engine. Evaluation on a particular kind can be set by setting interpreted = true when calling addFunctionKind.

11 years agoMinor cleanup of sources
Morgan Deters [Tue, 12 Feb 2013 04:56:10 +0000 (23:56 -0500)]
Minor cleanup of sources