cvc5.git
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

11 years agoFixes for miplib-trick application (and a new testcase)
Morgan Deters [Fri, 8 Feb 2013 15:57:38 +0000 (10:57 -0500)]
Fixes for miplib-trick application (and a new testcase)

11 years agoRemove PropositionalQuery class and all CUDD-related build stuff (and references)
Morgan Deters [Thu, 31 Jan 2013 19:29:58 +0000 (14:29 -0500)]
Remove PropositionalQuery class and all CUDD-related build stuff (and references)

11 years agoMinor fixes to build system
Morgan Deters [Tue, 19 Mar 2013 19:07:46 +0000 (15:07 -0400)]
Minor fixes to build system

11 years agoadded the cpp file for the inequality graph
Liana Hadarean [Tue, 19 Mar 2013 18:25:56 +0000 (14:25 -0400)]
added the cpp file for the inequality graph

11 years agoimplementing more inequality graph stuff; work in progress doesn't compile
Liana Hadarean [Tue, 19 Mar 2013 04:51:17 +0000 (00:51 -0400)]
implementing more inequality graph stuff; work in progress doesn't compile

11 years agomore work on inequality reasoning for bv
lianah [Mon, 18 Mar 2013 23:10:47 +0000 (19:10 -0400)]
more work on inequality reasoning for bv

11 years agostarted work on the inequality bv subtheory
lianah [Sat, 16 Mar 2013 19:48:51 +0000 (15:48 -0400)]
started work on the inequality bv subtheory

11 years agoBoolean terms rewriting for quantified variables of type Bool, when quantifier body...
Morgan Deters [Fri, 15 Mar 2013 17:30:05 +0000 (13:30 -0400)]
Boolean terms rewriting for quantified variables of type Bool, when quantifier body uses them in term context

11 years agoMerge branch '1.0.x'
Morgan Deters [Fri, 15 Mar 2013 16:34:58 +0000 (12:34 -0400)]
Merge branch '1.0.x'

11 years agofix up build system for swig (d242c30 introduced a subtle error)
Morgan Deters [Fri, 15 Mar 2013 16:34:52 +0000 (12:34 -0400)]
fix up build system for swig (d242c30 introduced a subtle error)

11 years agochanged default option for quantifier instantiation
Andrew Reynolds [Fri, 15 Mar 2013 14:15:23 +0000 (09:15 -0500)]
changed default option for quantifier instantiation

11 years agoMerge branch '1.0.x'
Morgan Deters [Thu, 14 Mar 2013 21:27:19 +0000 (17:27 -0400)]
Merge branch '1.0.x'

11 years agoFix warning (line annotation)
Morgan Deters [Thu, 14 Mar 2013 21:23:43 +0000 (17:23 -0400)]
Fix warning (line annotation)

11 years agofix to build system: #include the proper file when they are in both builds and src
Morgan Deters [Thu, 14 Mar 2013 21:16:02 +0000 (17:16 -0400)]
fix to build system: #include the proper file when they are in both builds and src

11 years agoAdded a rewrite for iff:
Clark Barrett [Thu, 14 Mar 2013 00:37:57 +0000 (20:37 -0400)]
Added a rewrite for iff:
x = c iff x = d ---> false
This fixes Andy's problem if unconstrained simplification is turned on.

11 years agopost failed attempts at getting the incremental solver to work
lianah [Wed, 13 Mar 2013 17:44:33 +0000 (13:44 -0400)]
post failed attempts at getting the incremental solver to work

11 years agoite removal option for quantifiers --ite-remove-quant, e-matching for boolean terms...
Andrew Reynolds [Mon, 11 Mar 2013 21:29:22 +0000 (16:29 -0500)]
ite removal option for quantifiers --ite-remove-quant, e-matching for boolean terms, improvement for pre skolemization

11 years agoDisallow overflow in bitvector literals (parser only)
Morgan Deters [Fri, 22 Feb 2013 21:48:13 +0000 (16:48 -0500)]
Disallow overflow in bitvector literals (parser only)

* For example, (_ bv5 1) is now an error instead of being silently truncated.
* Probably inappropriate for 1.0.x because it changes exception specifications.

11 years agomore slicer changes for incremental
lianah [Wed, 6 Mar 2013 21:35:38 +0000 (16:35 -0500)]
more slicer changes for incremental

11 years agoBest heuristics for handling decision requests from arrays
Clark Barrett [Wed, 6 Mar 2013 19:17:43 +0000 (14:17 -0500)]
Best heuristics for handling decision requests from arrays

11 years agofixed two bugs for the new E-matching implementation, added aggressive miniscoping...
Andrew Reynolds [Wed, 6 Mar 2013 16:46:07 +0000 (10:46 -0600)]
fixed two bugs for the new E-matching implementation, added aggressive miniscoping option --ag-miniscope-quant, minor cleanup

11 years agoMerge branch '1.0.x'
Morgan Deters [Tue, 5 Mar 2013 22:49:25 +0000 (17:49 -0500)]
Merge branch '1.0.x'

Conflicts:
src/smt/smt_engine.cpp

11 years agoBugfix for SmtEngine: proper unsubscribing for NodeManager events
Morgan Deters [Tue, 5 Mar 2013 00:58:09 +0000 (19:58 -0500)]
Bugfix for SmtEngine: proper unsubscribing for NodeManager events

11 years agoMerge branch '1.0.x'
Morgan Deters [Fri, 1 Mar 2013 23:28:22 +0000 (18:28 -0500)]
Merge branch '1.0.x'

11 years agoBug fix for rep-set.
Morgan Deters [Tue, 26 Feb 2013 21:41:56 +0000 (16:41 -0500)]
Bug fix for rep-set.

(Cherry-picked from commit c71ec27 in master.)

11 years agoFix for quantifiers containing Boolean terms.
Morgan Deters [Fri, 22 Feb 2013 15:52:46 +0000 (10:52 -0500)]
Fix for quantifiers containing Boolean terms.

11 years agoMerge branch '1.0.x'
lianah [Tue, 26 Feb 2013 21:02:52 +0000 (16:02 -0500)]
Merge branch '1.0.x'

11 years agoMerge branch '1.0.x' of https://github.com/CVC4/CVC4 into 1.0.x
lianah [Tue, 26 Feb 2013 20:50:48 +0000 (15:50 -0500)]
Merge branch '1.0.x' of https://github.com/CVC4/CVC4 into 1.0.x

11 years agofix for bv crash in incremental mode; this is a temporary fix for bug 493
lianah [Tue, 26 Feb 2013 20:50:37 +0000 (15:50 -0500)]
fix for bv crash in incremental mode; this is a temporary fix for bug 493

11 years agoadded option --model-u-dt-enum for outputting uninterpreted sorts as datatype enumera...
Andrew Reynolds [Sun, 24 Feb 2013 22:37:46 +0000 (16:37 -0600)]
added option --model-u-dt-enum for outputting uninterpreted sorts as datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts

11 years agoSingle -q quiets messages/warnings. Double -qq silences sat/unsat output too.
Morgan Deters [Sat, 16 Feb 2013 20:35:16 +0000 (15:35 -0500)]
Single -q quiets messages/warnings.  Double -qq silences sat/unsat output too.

11 years agoSome exception specification fixes in SmtEngine/Command infrastructure
Morgan Deters [Wed, 20 Feb 2013 23:09:59 +0000 (18:09 -0500)]
Some exception specification fixes in SmtEngine/Command infrastructure

11 years agoFix for gitinfo (resolves bug 399).
Morgan Deters [Mon, 18 Feb 2013 16:04:43 +0000 (11:04 -0500)]
Fix for gitinfo (resolves bug 399).

11 years agoMerge branch '1.0.x'
Kshitij Bansal [Sun, 17 Feb 2013 04:57:57 +0000 (23:57 -0500)]
Merge branch '1.0.x'

11 years agogitinfo modifications fix
Kshitij Bansal [Sun, 17 Feb 2013 04:56:22 +0000 (23:56 -0500)]
gitinfo modifications fix

11 years agoMerge pull request #6 from kbansal/decNewoptions
Kshitij Bansal [Sun, 17 Feb 2013 03:28:14 +0000 (19:28 -0800)]
Merge pull request #6 from kbansal/decNewoptions

decision/ code refactoring

11 years agodecision: jh: more refactoring (.h->.cpp, xor/iff)
Kshitij Bansal [Sun, 17 Feb 2013 01:52:03 +0000 (20:52 -0500)]
decision: jh: more refactoring (.h->.cpp, xor/iff)

11 years agodecision/ : jh: refactor embedded ITE, other minor
Kshitij Bansal [Sun, 17 Feb 2013 00:58:07 +0000 (19:58 -0500)]
decision/ : jh: refactor embedded ITE, other minor

other minor: cleanup some remaning fragments of GiveUpException(),
hopefully all is gone now.