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

8 years agoRefactoring Options Handler & Library Cycle Breaking
Tim King [Tue, 15 Dec 2015 02:51:40 +0000 (18:51 -0800)]
Refactoring Options Handler & Library Cycle Breaking

What to Know As a User:
A number of files have moved. Users that include files in the public API in more refined ways than using #include <cvc4.h> should consult which files have moved. Note though that some files may move again after being cleaned up. A number of small tweaks have been made to the swig interfaces that may cause issues. Please file bug reports for any problems.

The Problem:
The build order of CVC4 used to be [roughly] specified as:
  options < expr < util < libcvc4 < parsers < main
Each of these had their own directories and their own Makefile.am files. With the exception of the util/ directory, each of the subdirectories built exactly one convenience library. The util/ directory additionally built a statistics library. While the order above was partially correct, the build order was more complicated as options/Makefile.am executed building the sources for expr/Makefile.am as part of its BUILT_SOURCES phase. This options/Makefile.am also build the options/h and options.cpp files in other directories. There were cyclical library dependencies between the first four above libraries. All of these aspects combined to make options extremely brittle and hard to develop. Maintaining these between clang versus gcc, and bazel versus autotools has become increasing unpredictable.

The Solution:
To address these cyclic build problems, I am simplifying the build process. Here are the main things that have to happen:
1. util/ will be split into 3 separate directories: base, util, and smt_util. Each will have their own library and Makefile.am file.
2. Dependencies for options/ will be moved into options/. If a type appears as an option, this file will be moved into options.
3. All of the old options_handlers.h files have been refactored.
4. Some files have moved from util into expr/ to resolve cycles. Some of these moves are temporary.
5. I am removing the libstatistics library.

The constraints that the CVC4 build system will eventually satisfy are:
- The include order for both the .h and .cpp files for a directory must respect the order libraries are built. For example, a file in options/ cannot include from the expr/ directory. This includes built source files such as those coming from */kinds files and */options files.
- The types definitions must also respect the build order. Forward type declarations will be allowed in exceptional, justified cases.
- The Makefile.am for a directory cannot generate a file outside of the directory it controls. (Or call another Makefile.am except through subdirectory calls.)
- One library per Makefile.am.
- No extra copies of libraries will be built for the purpose of distinguishing between external and internal visibility in libraries for building parser/ or main/ libraries and binaries. Any function used by parser/ and main/ will be labeled with CVC4_PUBLIC and be in a public API. (AFAICT, libstatistics was being built exactly to skirt this.)

The build order of CVC4 can now be [roughly] specified as
  base < options < util < expr < smt_util < libcvc4 < parsers < main
The distinction between "base < options < util < expr" are currently clean. The relationship between expr and the subsequent directories/libraries are not yet clean.

More details about the directories:

base/
The new directory base/ contains the shared utilities that are absolutely crucial to starting cvc4. The list currently includes just: cvc4_assert.{h,cpp}, output.{h,cpp}, exception.{h,cpp}, and tls.{h, h.in, cpp}. These are things that are required everywhere.

options/
The options/ directory is self contained.
- It contains all of the enums that appear as options. This includes things like theory/bv/bitblast_mode.h .
- There are exactly 4 classes that handled currently using forward declarations currently to this: LogicInfo, LemmaInputChannel, LemmaOutputChannel, and CommandSequence. These will all be removed from options.
- Functionality of the options_handlers.h files has been moved into smt/smt_options_handler.h. The options library itself only uses an interface class defined in options/options_handler_interface.h. We are now using virtual dispatch to avoid using inlined functions as was previously done.
- The */options_handlers.h files have been removed.
- The generated smt/smt_options.cpp file has been be replaced by pushing the functionality that was generated into: options/options_handler_{get,set}_option_template.cpp . The non-generated functionality was moved into smt_engine.cpp.
- All of the options files have been moved from their directories into options/. This means includes like theory/arith/options.h have changed to change to options/arith_options.h .

util/
The util/ directory continues to contain core utility classes that may be used [almost] everywhere. The exception is that these are not used by options/ or base/. This includes things like rational and integer. These may not use anything in expr/ or libcvc4. A number of files have been moved out of this directory as they have cyclic dependencies graph with exprs and types. The build process up to this directory is currently clean.

expr/
The expr/ directory continues to be the home of expressions. The major change is files moving from util/ moving into expr/. The reason for this is that these files form a cycle with files in expr/.
- An example is datatype.h. This includes "expr/expr.h", "expr/type.h" while "expr/command.h" includes datatype.h.
- Another example is predicate.h. This uses expr.h and is also declared in a kinds file and thus appears in kinds.h.
- The rule of thumb is if expr/ pulls it in it needs to be independent of expr/, in which case it is in util/, or it is not, in which case it is pulled into expr/.
- Some files do not have a strong justification currently. Result, ResourceManager and SExpr can be moved back into util/ once the iostream manipulation routines are refactored out of the Node and Expr classes.
- Note the kinds files are expected to remain in the theory/ directories. These are only read in order to build sources.
- This directory is not yet clean. It contains forward references into libcvc4 such as the printer. It also makes some classes used by main/ and parser CVC4_PUBLIC.

smt_util/
The smt_util/ directory contains those utility classes which require exprs, but expr/ does not require them. These are mostly utilities for working with expressions and nodes. Examples include ite_removal.h, LemmaInputChannel and LemmaOutputChannel.

What is up next:
- A number of new #warning "TODO: ..." items have been scattered throughout the code as reminders to myself. Help with these issues is welcomed.
- The expr/ directory needs to be cleaned up in a similar to options/. Before this happens statistics needs to be cleaned up.

8 years agoAdd option fmf-empty-sorts.
ajreynol [Thu, 10 Dec 2015 12:32:42 +0000 (13:32 +0100)]
Add option fmf-empty-sorts.

8 years agoReverting a previous change to the options_handlers.h. Using inline defintions again...
Tim King [Fri, 4 Dec 2015 04:46:48 +0000 (23:46 -0500)]
Reverting a previous change to the options_handlers.h. Using inline defintions again to better handle a circular dependency.

8 years agoRemoving the generated directory from the parsers.
Tim King [Thu, 3 Dec 2015 21:54:15 +0000 (13:54 -0800)]
Removing the generated directory from the parsers.

8 years agoModifying the src/options/Makefile.am for travis.
Tim King [Thu, 3 Dec 2015 06:33:26 +0000 (01:33 -0500)]
Modifying the src/options/Makefile.am for travis.

8 years agoModifying options/Makefile.am to pass distcheck. There is an unpleasant hack in this...
Tim King [Thu, 3 Dec 2015 05:29:39 +0000 (21:29 -0800)]
Modifying options/Makefile.am to pass distcheck. There is an unpleasant hack in this fix.

8 years agoAdds Google, Inc. to the AUTHORS file.
Chris Conway [Wed, 2 Dec 2015 21:56:52 +0000 (13:56 -0800)]
Adds Google, Inc. to the AUTHORS file.

8 years agoMinor fixes for cegqi-si-partial.
ajreynol [Wed, 2 Dec 2015 16:45:07 +0000 (17:45 +0100)]
Minor fixes for cegqi-si-partial.

8 years agoSeparating the steps of the old mkoptions script into smaller phases.
Tim King [Tue, 1 Dec 2015 06:55:26 +0000 (01:55 -0500)]
Separating the steps of the old mkoptions script into smaller phases.

8 years agoGuarding the destruction of the a linux specific variable on WIN32.
Tim King [Sat, 28 Nov 2015 05:28:43 +0000 (00:28 -0500)]
Guarding the destruction of the a linux specific variable on WIN32.

8 years agoMerge pull request #79 from CVC4/fix-mac-build-script
Tim King [Wed, 2 Dec 2015 04:54:15 +0000 (20:54 -0800)]
Merge pull request #79 from CVC4/fix-mac-build-script

Adds required steps to contrib/mac-build.