cvc5.git
8 years agoMerge remote-tracking branch 'origin/master'
PaulMeng [Sat, 25 Jun 2016 22:20:30 +0000 (18:20 -0400)]
Merge remote-tracking branch 'origin/master'

8 years agotest
PaulMeng [Sat, 25 Jun 2016 21:55:09 +0000 (17:55 -0400)]
test

8 years agoreimplemented std effort for TC
PaulMeng [Sat, 25 Jun 2016 21:55:09 +0000 (17:55 -0400)]
reimplemented std effort for TC

8 years agochange to use tuple element representatives to build TC graph for full
PaulMeng [Thu, 5 May 2016 19:58:10 +0000 (14:58 -0500)]
change to use tuple element representatives to build TC graph for full
effort

8 years agoimplemented TC for standard effort
PaulMeng [Wed, 4 May 2016 15:21:18 +0000 (10:21 -0500)]
implemented TC for standard effort

8 years agoupdate from the master
PaulMeng [Wed, 20 Apr 2016 19:43:18 +0000 (14:43 -0500)]
update from the master

8 years agoadd utils class for relational theory
PaulMeng [Wed, 20 Apr 2016 18:54:32 +0000 (13:54 -0500)]
add utils class for relational theory

8 years agoRefactored code
PaulMeng [Wed, 20 Apr 2016 03:51:30 +0000 (22:51 -0500)]
Refactored code

8 years agochange transitive closure operator name to TCLOUSRE
PaulMeng [Fri, 15 Apr 2016 16:40:40 +0000 (11:40 -0500)]
change transitive closure operator name to TCLOUSRE

8 years ago- Implement constant rewriter for relational operators for model generation
PaulMeng [Fri, 15 Apr 2016 03:01:32 +0000 (22:01 -0500)]
- Implement constant rewriter for relational operators for model generation
- fixed a few bugs

8 years agoadded more benchmarks
PaulMeng [Tue, 12 Apr 2016 15:05:42 +0000 (10:05 -0500)]
added more benchmarks

8 years agofixed explanation for transitive closure inferences
PaulMeng [Tue, 12 Apr 2016 15:02:26 +0000 (10:02 -0500)]
fixed explanation for transitive closure inferences

8 years agoimplement standard effort support for product
PaulMeng [Thu, 7 Apr 2016 19:55:17 +0000 (14:55 -0500)]
implement standard effort support for product

8 years ago- added standard effort for transpose
PaulMeng [Thu, 7 Apr 2016 18:41:21 +0000 (13:41 -0500)]
- added standard effort for transpose
- implement transitive closure rule for concrete input

8 years agoadded typing rule for transitive closure
PaulMeng [Wed, 23 Mar 2016 14:15:17 +0000 (09:15 -0500)]
added typing rule for transitive closure

8 years agominor fix
PaulMeng [Tue, 22 Mar 2016 15:30:46 +0000 (10:30 -0500)]
minor fix

8 years agominor fix
PaulMeng [Tue, 22 Mar 2016 02:09:27 +0000 (21:09 -0500)]
minor fix

8 years agominor fix
PaulMeng [Fri, 11 Mar 2016 17:25:51 +0000 (11:25 -0600)]
minor fix

8 years agominor fix
PaulMeng [Thu, 10 Mar 2016 21:31:19 +0000 (15:31 -0600)]
minor fix

8 years agofixed the transpose-occur rule
PaulMeng [Thu, 10 Mar 2016 20:34:26 +0000 (14:34 -0600)]
fixed the transpose-occur rule

8 years agomake skolems and tuple reduction terms as shared terms
PaulMeng [Wed, 9 Mar 2016 01:26:13 +0000 (19:26 -0600)]
make skolems and tuple reduction terms as shared terms

- added more benchmarks for pressure and theory combination tests
- fixed find terms method in trie data structure
- use a separate membership map to store positive membership terms

8 years agomodified CVC4 native language parser to accept 1-tuple declaration:
PaulMeng [Mon, 7 Mar 2016 20:30:36 +0000 (14:30 -0600)]
modified CVC4 native language parser to accept 1-tuple declaration:
TUPLE(1)

- fixed the tuple element selection for product-split and join-split
rules

8 years agorefactored the code
PaulMeng [Fri, 4 Mar 2016 17:27:02 +0000 (11:27 -0600)]
refactored the code

- send out facts as lemmas
- fixed the non-termination problem caused by sending facts as lemmas
- unfolded symbolic tuples by adding equality lemmas

8 years agosmall fixes for eq rep names
PaulMeng [Tue, 1 Mar 2016 20:36:36 +0000 (14:36 -0600)]
small fixes for eq rep names

8 years agosmall fix for naming
PaulMeng [Tue, 1 Mar 2016 20:22:35 +0000 (14:22 -0600)]
small fix for naming

8 years agofixed product rules
PaulMeng [Tue, 1 Mar 2016 20:17:08 +0000 (14:17 -0600)]
fixed product rules

8 years agoadapted the solver to accept sets of built-in types (int, string, real)
PaulMeng [Tue, 1 Mar 2016 05:23:50 +0000 (23:23 -0600)]
adapted the solver to accept sets of built-in types (int, string, real)

use dummy lemmas to find tuple elements equality

8 years agoAdded more benchmarks
PaulMeng [Mon, 29 Feb 2016 17:10:01 +0000 (11:10 -0600)]
Added more benchmarks
Fixed the problem that duplicates and split facts were sent as lemmas
causing nontermination
Fixed the computation of join and product relations without simplication

8 years agoimplemented a basic solving procedure for finite relations (only for
PaulMeng [Sun, 28 Feb 2016 22:22:43 +0000 (16:22 -0600)]
implemented a basic solving procedure for finite relations (only for
join, product, transpose operators)

8 years agoadded rules for join and transpose operators
PaulMeng [Wed, 17 Feb 2016 21:01:40 +0000 (15:01 -0600)]
added rules for join and transpose operators
added more benchmarks

8 years agoMerge remote-tracking branch 'origin/master'
PaulMeng [Mon, 15 Feb 2016 23:41:56 +0000 (17:41 -0600)]
Merge remote-tracking branch 'origin/master'

8 years agoextended smt parser for the finite relations
PaulMeng [Mon, 15 Feb 2016 23:36:07 +0000 (17:36 -0600)]
extended smt parser for the finite relations
fixed typing rules for relational terms
added a benchmark example for the theory of finite relations

8 years agoMinor change to last commit
ajreynol [Mon, 15 Feb 2016 19:38:51 +0000 (13:38 -0600)]
Minor change to last commit

8 years agoEliminate most of the internal representation infrastructure for tuples and records...
ajreynol [Mon, 15 Feb 2016 19:02:02 +0000 (13:02 -0600)]
Eliminate most of the internal representation infrastructure for tuples and records, replace with datatypes throughout, update cvc printer for tuples/records.  Minor changes to API for records and tuples.

8 years agoMore aggressive conditional rewriting for quantified formulas. Bug fix set incomplete...
ajreynol [Thu, 11 Feb 2016 21:07:37 +0000 (15:07 -0600)]
More aggressive conditional rewriting for quantified formulas. Bug fix set incomplete for fmc.

8 years agoFix model postprocessor for tuples, add regression.
ajreynol [Wed, 10 Feb 2016 16:17:18 +0000 (10:17 -0600)]
Fix model postprocessor for tuples, add regression.

8 years agoFix regression, minor change to output.
ajreynol [Tue, 9 Feb 2016 22:57:50 +0000 (16:57 -0600)]
Fix regression, minor change to output.

8 years ago- extend cvc4 frontend parser to accept relational operators (product,
PaulMeng [Tue, 9 Feb 2016 20:51:44 +0000 (14:51 -0600)]
- extend cvc4 frontend parser to accept relational operators (product,
join, transpose, transitive closure)
- added a finite relations module to collect all relational terms in EE

8 years agoEager introduction of eqc, lemma cache for ground fmf. Apply preprocessing to quantif...
ajreynol [Tue, 9 Feb 2016 19:23:18 +0000 (13:23 -0600)]
Eager introduction of eqc, lemma cache for ground fmf. Apply preprocessing to quantifier instantiations.

8 years agoUpdates related to finite model finding and (co)datatypes. Bug fix enumerator and...
ajreynol [Mon, 8 Feb 2016 21:49:14 +0000 (15:49 -0600)]
Updates related to finite model finding and (co)datatypes. Bug fix enumerator and codatatype rewriter, further simplify fmc.

8 years agoChanging the way the equality engine explains disequalities.
guykatzz [Sat, 6 Feb 2016 00:10:36 +0000 (16:10 -0800)]
Changing the way the equality engine explains disequalities.

The explanation for a != b is now:
1. a == find(a)
2. ( find(a) == find(b) ) == false
3. find(b) == b

This simplifies the creation of transitivity proofs for disequalities.

8 years agoAdd two optimizations for datatypes, currently disabled. Bug fix rewriter for selecto...
ajreynol [Fri, 5 Feb 2016 16:24:49 +0000 (10:24 -0600)]
Add two optimizations for datatypes, currently disabled. Bug fix rewriter for selectors applied to codatatype values.

8 years agoFixed two more memory leaks in array_info.cpp
Clark Barrett [Thu, 4 Feb 2016 21:57:26 +0000 (13:57 -0800)]
Fixed two more memory leaks in array_info.cpp

8 years agoAdded --omit-dont-cares option which doesn't print model values for
Clark Barrett [Wed, 3 Feb 2016 22:04:27 +0000 (14:04 -0800)]
Added --omit-dont-cares option which doesn't print model values for
variables known to be don't-cares.

8 years agoMoving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. Breaking...
Tim King [Tue, 2 Feb 2016 17:47:34 +0000 (09:47 -0800)]
Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. Breaking an edge between the sat solver and command.h.

8 years agoRemoving the CVC4_PUBLIC attribute from the forward declaration of Record in type.h.
Tim King [Mon, 1 Feb 2016 19:45:14 +0000 (11:45 -0800)]
Removing the CVC4_PUBLIC attribute from the forward declaration of Record in type.h.

8 years agoRemoving the CVC4_NEEDS_REPLACEMENT_FUNCTIONS guard to have a simpler build process.
Tim King [Mon, 1 Feb 2016 19:43:31 +0000 (11:43 -0800)]
Removing the CVC4_NEEDS_REPLACEMENT_FUNCTIONS guard to have a simpler build process.

8 years agoGeneralizing lib/strtok_r.c so that it can always be compiled.
Tim King [Mon, 1 Feb 2016 19:29:49 +0000 (11:29 -0800)]
Generalizing lib/strtok_r.c so that it can always be compiled.

8 years agoGeneralizing the implementation of lib/clock_gettime.c so that it can always be compiled.
Tim King [Mon, 1 Feb 2016 19:28:33 +0000 (11:28 -0800)]
Generalizing the implementation of lib/clock_gettime.c so that it can always be compiled.

8 years agoFixing a potentially malformed template expansion when Dump() is disabled.
Tim King [Mon, 1 Feb 2016 19:25:29 +0000 (11:25 -0800)]
Fixing a potentially malformed template expansion when Dump() is disabled.

8 years agoFixing a memory leak in bv_subtheory_algebraic.cpp. Also formatting the file.
Tim King [Mon, 1 Feb 2016 19:22:12 +0000 (11:22 -0800)]
Fixing a memory leak in bv_subtheory_algebraic.cpp. Also formatting the file.

8 years agoAdding an virtual destructor to OstreamUpdate.
Tim King [Mon, 1 Feb 2016 19:12:10 +0000 (11:12 -0800)]
Adding an virtual destructor to OstreamUpdate.

8 years agoMaking the ManagedOstream::defaultSource() a const function.
Tim King [Mon, 1 Feb 2016 19:10:51 +0000 (11:10 -0800)]
Making the ManagedOstream::defaultSource() a const function.

8 years agoAdding a destructor to ProofOutputChannel.
Tim King [Mon, 1 Feb 2016 19:09:09 +0000 (11:09 -0800)]
Adding a destructor to ProofOutputChannel.

8 years agoFixing white spaces in sat_proof.h.
Tim King [Mon, 1 Feb 2016 19:07:41 +0000 (11:07 -0800)]
Fixing white spaces in sat_proof.h.

8 years agoMaking the references to std more explicit in didyoumean.cpp.
Tim King [Mon, 1 Feb 2016 18:59:49 +0000 (10:59 -0800)]
Making the references to std more explicit in didyoumean.cpp.

8 years agoFixing a memory leak in array info.
Tim King [Mon, 1 Feb 2016 18:56:55 +0000 (10:56 -0800)]
Fixing a memory leak in array info.

8 years agoDeleting the dead code in proof/sat_proof.cpp.
Tim King [Mon, 1 Feb 2016 18:54:45 +0000 (10:54 -0800)]
Deleting the dead code in proof/sat_proof.cpp.

8 years agoSimplify fmc model construction, add regression. Improve FMF debug assertions.
ajreynol [Mon, 1 Feb 2016 17:18:00 +0000 (11:18 -0600)]
Simplify fmc model construction, add regression. Improve FMF debug assertions.

8 years agoAdding listeners to Options.
Tim King [Thu, 28 Jan 2016 20:35:45 +0000 (12:35 -0800)]
Adding listeners to Options.
- Options
-- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options.
-- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners.
-- Added functions to Options for registering listeners of the notify calls.
-- Changed a number of options to use the new listener infrastructure.
-- Fixed a number of warnings in options.
-- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure.
-- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}.

- Theories
-- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options.

- Ostream Handling:
-- Added new functionality that generalized how ostreams are opened, options/open_stream.h.
-- Simplified the memory management for different ostreams, smt/managed_ostreams.h.
-- Had the SmtEnginePrivate manage the memory for the ostreams set by options.
-- Simplified how the setting of ostreams are updated, smt/update_ostream.h.

- Configuration and Tags:
-- Configuration can now be used during predicates and handlers for options.
-- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/.
-- Moved {Debug,Trace}_tags.* from being generated in options/ into base/.

- cvc4_private.h
-- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's.
-- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations.
-- Made lib/lib/clock_gettime.h a cvc4_private_library.h header.

- Antlr
-- Fixed antlr and cvc4 macro definition conflicts that caused warnings.

- SmtGlobals
-- Refactored replayStream and replayLog out of SmtGlobals.
-- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.

8 years agoMerged bit-vector and uf proof branch.
Liana Hadarean [Wed, 27 Jan 2016 00:04:26 +0000 (16:04 -0800)]
Merged bit-vector and uf proof branch.

8 years agoFix bug in fmc mbqi where modelscomputed for mbqi could involve non-constant values...
ajreynol [Wed, 20 Jan 2016 22:55:02 +0000 (16:55 -0600)]
Fix bug in fmc mbqi where modelscomputed for mbqi could involve non-constant values. Add regression.

8 years agoBug fixes for model construction with codatatypes, add regressions.
ajreynol [Tue, 19 Jan 2016 18:21:50 +0000 (12:21 -0600)]
Bug fixes for model construction with codatatypes, add regressions.

8 years agoBug fix rewriter for fun defs.
ajreynol [Mon, 18 Jan 2016 21:33:22 +0000 (22:33 +0100)]
Bug fix rewriter for fun defs.

8 years agoType enumerators take optional argument indicating fixed cardinalities of uninterpret...
ajreynol [Fri, 15 Jan 2016 22:57:56 +0000 (23:57 +0100)]
Type enumerators take optional argument indicating fixed cardinalities of uninterpreted sorts. Modify TheoryModelBuilder.  Fix bug in fmf-empty-sorts.

8 years agoEnsure model construction for parametric sorts involving uninterpreted sorts respect...
ajreynol [Thu, 14 Jan 2016 23:18:49 +0000 (00:18 +0100)]
Ensure model construction for parametric sorts involving uninterpreted sorts respect cardinality bounds on when finite model finding is enabled.

8 years agoLemma cache datatypes. Do not send true lemma in quantifiers. Minor fix for datatypes...
ajreynol [Wed, 13 Jan 2016 22:08:40 +0000 (23:08 +0100)]
Lemma cache datatypes. Do not send true lemma in quantifiers. Minor fix for datatypes model generation for UFinite datatypes when FMF.

8 years agoAdding a new Listener utility class. Changing the ResourceManager to use Listeners...
Tim King [Sat, 9 Jan 2016 02:19:30 +0000 (18:19 -0800)]
Adding a new Listener utility class. Changing the ResourceManager to use Listeners for reporting hard and soft resource out() events.

8 years agoRemoving StatisticsRegistry's static functions current() and registerStat().
Tim King [Sat, 9 Jan 2016 00:44:57 +0000 (16:44 -0800)]
Removing StatisticsRegistry's static functions current() and registerStat().
- The functionality the get the StatisticsRegistry attached to the SmtEngine was previously through StatisticsRegistry::current(). This is the dominant StatisticsRegistry in the code. (There is another StatisticsRegistry attached to the NodeManager.) Having this be a static function on StatisticsRegistry requires the use of an SmtEngine in the wrong compilation unit.
- Usages of StatisticsRegistry::current() that were visible in prop/{bvminisat,minisat} has been removed. A pointer to the relevant StatisticsRegistry should be passed instead into the constructor.
- The function StatisticsRegistry::current() has been replaced by SmtScope::currentStatisticsRegistry(). SmtScope is in the libcvc4 package, where SmtEngine is available in the compilation unit.
- The function smtStatisticsRegistry() is a synonym for SmtScope::currentStatisticsRegistry() in smt/smt_statistics_registry.h. This header has fewer include dependencies than the one for SmtScope.
- Correspondingly, the static functions StatisticsRegistry::{registerStat, unregisterStat} have been removed. One should instead use smtStatisticsRegistry()->{registerStat,unregisterStat} instead.
- The KEEP_STATISTIC macro has been moved into smt/smt_statistics_registry.h.
- Documents the reason StatisticsRegistry is CVC4_PUBLIC. This lets me remove the warning I added.
- Removing most operators for timespec from statistics_registry.h file. These a bit error prone in clang.
- Most of the really confusing ifdef's in util/statistics_registry.h are gone.

8 years agoDisabling the RESTART command.
Tim King [Fri, 8 Jan 2016 06:39:41 +0000 (01:39 -0500)]
Disabling the RESTART command.

8 years agofix windows builds
Kshitij Bansal [Wed, 6 Jan 2016 21:02:50 +0000 (16:02 -0500)]
fix windows builds

8 years agoFixing a SWIG ordering issue between bitvector and integer.
Tim King [Wed, 6 Jan 2016 20:43:41 +0000 (12:43 -0800)]
Fixing a SWIG ordering issue between bitvector and integer.

8 years agoImproving the documentation of the CVC command CONTINUE.
Tim King [Wed, 6 Jan 2016 08:10:36 +0000 (00:10 -0800)]
Improving the documentation of the CVC command CONTINUE.

8 years agoRemoving dead code. StackingMap only appeared in unit tests.
Tim King [Wed, 6 Jan 2016 01:35:12 +0000 (17:35 -0800)]
Removing dead code. StackingMap only appeared in unit tests.

8 years agoMoving sexpr.{cpp,h,i} from expr/ back into util/.
Tim King [Wed, 6 Jan 2016 01:28:38 +0000 (17:28 -0800)]
Moving sexpr.{cpp,h,i} from expr/ back into util/.

8 years agoAdd SmtGlobals Class
Tim King [Wed, 6 Jan 2016 00:29:44 +0000 (16:29 -0800)]
Add SmtGlobals Class
- The options replayStream, lemmaInputChannel, lemmaOutputChannel have been removed due to their datatypes. These datatypes were previously pointers to types that were not usable from the options/ library.
- The option replayLog has been removed due to inconsistent memory management.
- SmtGlobals is a class that wraps a pointer to each of these removed options. These can each be set independently.
- There is a single SmtGlobals per SmtEngine with the lifetime of the SmtEngine.
- A pointer to this is freely given to the user of an SmtEngine to parameterize the solver after construction.
- Selected classes have been given a copy of this pointer in their constructors.
- Removed the dependence on Node from Result. Moving Result back into util/.

8 years agoAdding a new class LastExceptionBuffer for the purpose of owning the memory for the...
Tim King [Tue, 5 Jan 2016 19:36:30 +0000 (11:36 -0800)]
Adding a new class LastExceptionBuffer for the purpose of owning the memory for the last exception C string. This replaces s_debugLastException.

8 years agoAdded propagation rule for array ext lemmas to aid proofs
Clark Barrett [Fri, 1 Jan 2016 20:30:04 +0000 (12:30 -0800)]
Added propagation rule for array ext lemmas to aid proofs

8 years agoModified tear-down-incremental option to take an integer - the integer is the
Clark Barrett [Thu, 31 Dec 2015 06:38:13 +0000 (22:38 -0800)]
Modified tear-down-incremental option to take an integer - the integer is the
number of times a check must be executed before the system is reset.

8 years agoShuffling around public vs. private headers
Tim King [Wed, 30 Dec 2015 19:45:37 +0000 (11:45 -0800)]
Shuffling around public vs. private headers
- Adding a script contrib/test_install_headers.h that tests whether one can include all cvc4_public headers. CVC4 can pass this test after this commit.
- Making lib/{clock_gettime.h,ffs.h,strtok_r.h} cvc4_private.
- Making prop/sat_solver_factory.h cvc4_private.
- Moving the expr iostream manipulators into their own files: expr_iomanip.{h,cpp}.
- Setting the generated *_options.h files back to being cvc4_private.
-- Removing the usage of options/expr_options.h from expr.h.
-- Removing the include of base_options.h from options.h.
- Cleaning up CPP macros in cvc4_public headers.
-- Changing the ROLL macro in floatingpoint.h into an inline function.
-- Removing the now unused flag -D__BUILDING_STATISTICS_FOR_EXPORT.

8 years agoAdding a missing header include for cvc4_assert.h in smt_engine_check_proof.cpp for...
Tim King [Tue, 29 Dec 2015 09:19:30 +0000 (04:19 -0500)]
Adding a missing header include for cvc4_assert.h in smt_engine_check_proof.cpp for when proofs are disabled.

8 years agoMerged my changes from experimental branch (new array decision procedure,
Clark Barrett [Sun, 27 Dec 2015 03:20:27 +0000 (19:20 -0800)]
Merged my changes from experimental branch (new array decision procedure,
translation to bit-vectors for QF_NIA).

8 years agoChanging the attribute on the forward declaration of SetType in emptyset.h. This...
Tim King [Thu, 24 Dec 2015 20:01:52 +0000 (15:01 -0500)]
Changing the attribute on the forward declaration of SetType in emptyset.h. This seems to give many fewer warnings.

8 years agoAdding a missing return on the new ArrayStoreAll::operator= .
Tim King [Thu, 24 Dec 2015 20:00:35 +0000 (15:00 -0500)]
Adding a missing return on the new ArrayStoreAll::operator= .

8 years agoMiscellaneous fixes
Tim King [Thu, 24 Dec 2015 10:38:43 +0000 (05:38 -0500)]
Miscellaneous fixes
- Splitting the two instances of CheckArgument. The template version is now always defined in base/exception.h and is available in a cvc4_public header. This version has lost its variadic version (due to swig not supporting va_list's). The CPP macro version has been renamed PrettyCheckArgument. (Taking suggestions for a better name.) This is now only defined in base/cvc4_assert.h. Only use this in cvc4_private headers and in .cpp files that can use cvc4_private headers. To use a variadic version of CheckArguments, outside of this scope, you need to duplicate this macro locally. See cvc3_compat.cpp for an example.
- Making fitsSignedInt() and fitsUnsignedInt() work more robustly for CLN on 32 bit systems.
- Refactoring ArrayStoreAll to avoid potential problems with circular header inclusions.
- Changing some headers to use iosfwd when possible.

8 years agoEnabled array propagation during lemma propagation - this should catch some
Clark Barrett [Wed, 23 Dec 2015 17:42:03 +0000 (09:42 -0800)]
Enabled array propagation during lemma propagation - this should catch some
conflicts that now require extra splitting.

8 years agoAdded extract.cpp example
Clark Barrett [Wed, 23 Dec 2015 16:56:15 +0000 (08:56 -0800)]
Added extract.cpp example

8 years agoBug fix uf-ss-totality.
ajreynol [Tue, 22 Dec 2015 13:23:19 +0000 (14:23 +0100)]
Bug fix uf-ss-totality.

8 years agoAlways split on constructor types for datatypes involving uninterpreted sorts when...
ajreynol [Tue, 22 Dec 2015 12:44:05 +0000 (13:44 +0100)]
Always split on constructor types for datatypes involving uninterpreted sorts when finite model finding is enabled, add regressions.

8 years agoBug fix for cbqi, do not use model values for terms involving non-enumerable sorts.
ajreynol [Tue, 22 Dec 2015 11:03:10 +0000 (12:03 +0100)]
Bug fix for cbqi, do not use model values for terms involving non-enumerable sorts.

8 years agoModifying emptyset.h and sexpr. Adding SetLanguage.
Tim King [Sat, 19 Dec 2015 01:19:07 +0000 (17:19 -0800)]
Modifying emptyset.h and sexpr. Adding SetLanguage.

- Modifies expr/emptyset.h to use SetType only as an incomplete type within expr/emptyset.h. This breaks the include cycle between expr/emptyset.h, expr/expr.h and expr/type.h.
- Refactors SExpr to avoid a potentially infinite cycle. This is likely overkill, but it works.
- Moving Expr::setlanguage and related utilities out of the Expr class and into their own file. This allows files in util/ to know the output language set on an ostream.

8 years agoMinor
ajreynol [Thu, 17 Dec 2015 12:41:42 +0000 (13:41 +0100)]
Minor

8 years agoRemoving the Record iterator from the swig interface. Moving the cvc4 autogen include...
Tim King [Wed, 16 Dec 2015 17:36:16 +0000 (12:36 -0500)]
Removing the Record iterator from the swig interface. Moving the cvc4 autogen include in interactive_shell.cpp.

8 years agoWork on purification for quantifiers, minor updates.
ajreynol [Wed, 16 Dec 2015 10:24:09 +0000 (11:24 +0100)]
Work on purification for quantifiers, minor updates.

8 years agoBreaking the include cycle between Record and Expr.
Tim King [Tue, 15 Dec 2015 22:35:34 +0000 (14:35 -0800)]
Breaking the include cycle between Record and Expr.

8 years agoAdding destructors for CDO an CDOhash_map in the restore() functions.
Tim King [Fri, 4 Dec 2015 23:58:19 +0000 (15:58 -0800)]
Adding destructors for CDO an CDOhash_map in the restore() functions.

8 years agoRemoving the build cycle for predicate.
Tim King [Tue, 15 Dec 2015 21:36:08 +0000 (13:36 -0800)]
Removing the build cycle for predicate.

8 years agoMoving SExpr(bool) out of the header into sexpr.cpp to be less verbose about the...
Tim King [Tue, 15 Dec 2015 21:29:49 +0000 (13:29 -0800)]
Moving SExpr(bool) out of the header into sexpr.cpp to be less verbose about the warning.

8 years agoMaking logic_info_forward.h a public header for now.
Tim King [Tue, 15 Dec 2015 18:33:55 +0000 (13:33 -0500)]
Making logic_info_forward.h a public header for now.

8 years agoAdd option uf-ss-fair-monotone. Minor cleanup and improvement of sort inference.
ajreynol [Tue, 15 Dec 2015 11:37:23 +0000 (12:37 +0100)]
Add option uf-ss-fair-monotone. Minor cleanup and improvement of sort inference.