| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
Dump("foo") << FooCommand(...);
now "dumps" the textual representation of the command (in the current
output language) to a file, IF dumping is on at configure-time, AND the
"muzzle" feature is off, AND the "foo" flag is turned on for the dump
stream during this run.
If it's a portfolio build, the above will also store the command in a
CommandSequence, IF the "foo" flag is turned on for the dump stream
during this run. This is done even if the muzzle is on.
This commit also cleans up some code that used the dump feature (in arrays,
particularly).
|
|
support incrementality.
Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.
Expected performance change negligible; slightly better on memory:
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!
|
|
* separated SatSolverInput interface class into two classes:
- TheoryProxy for the sat solver to communicate with the theories
- SatSolverInterface abstract class to communicate with the sat solver
* instead of using #ifdef typedef for SatClauses and SatLiterals, now there are CVC4 SatLiteral/SatClause types and mappings between them and the internal sat solver clause/literal representation
* added abstract classes for DPLLSatSolver and BVSatSolver different interfaces
Replaced TheoryBV with bitblasting implementation:
* all operators bitblasted
* only operator elimination rewrite rules so far
|
|
my previous checkin)
|
|
now supports propagating equalities when a slack variable corresponding to a difference of shared terms must be 0. Similarly disequalities are propagated when these variables cannot be zero.
|
|
|
|
Details here: http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_October_14,_2011#Resource.2Ftime_limiting_API
This will need more work, but it's a start.
Also implemented TheoryEngine::properPropagation().
Other minor things.
|
|
to model gen on booleans; and a little cleanup
|
|
preparation of user push/pop in SAT solver
|
|
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
|
|
comparison <http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2673&&p=5&reference_id=2637>
|
|
|
|
|
|
|
|
|
|
|
|
preregistration is now called during the conversion to cnf. This fixes bug 257.
|
|
* Makes Options an "omnipresent thread-local global" (like the notion
of the "current NodeManager" was already). Options::current() accesses
this structure.
* Removes Options from constructors and data structures everywhere
(this cleans up a lot of things).
* No longer uses StatisticsRegistry statically. An instance of the
registry is created and linked to a NodeManager.
* StatisticsRegistry::current() is similar to Options::current(), but
the pointer is stowed in the NodeManager (rather than stored)
* The static functions of StatisticsRegistry have been left, for backward
compatibility; they now use the "current" statistics registry.
* SmtEngine::getStatisticsRegistry() is a public accessor for the
registry; this is needed by main() to reach in and get the registry,
for flushing statistics at the end.
|
|
|
|
(propositional) assignment for theory atoms.
Fixed Debug/Trace as discussed in bug ticket #252 and on the mailing list.
This implementation leads to some compiler warnings in production builds,
but these will be corrected in coming days. There appears to be a small
speedup in the parser as a result of this fix:
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=1902&reference_id=1886&p=5
Cleaned up a few CD Boolean attribute things.
Various small fixes to coding guidelines / test coverage.
This commit:
* Resolves bug 252 (tracing not disabled in production builds)
* Resolves bug 254 (implement CDAttrHash<>::BitIterator::find())
|
|
|
|
not yet in d_checkSat.
|
|
done by way of the intermediate branch arith-prop-tmp. Both arith-prop-opt and arith-prop-tmp will now be phased out.
|
|
(wr propagation) splitter in arithmetic.
|
|
|
|
util/options.h,cpp
|
|
* Adding options --lazy-type-checking and --eager-type-checking
to control type checking in NodeBuilder, which can now be enabled
in production mode and disabled in debug mode
* Option --no-checking implies --no-type-checking
* Adding constructor SmtEngine(ExprManager* em) that uses default options
|
|
notifies the theory engine through its output channel); some cleanup; add a regression for bug #216
|
|
supported; work on Result type (biggest noticeable change is that CVC4 now outputs lowercase "sat" and "unsat"), Options class moved to src/smt, to allow for future work on runtime configuration via (set-option) command
|
|
(get-value ...) SMT-LIBv2 command. As per SMT-LIBv2 spec,
you must pass --interactive --produce-models on the command
line (although they don't currently make us do any extra
work). Closes bug #213.
|
|
should have no impact on production performance and speed up debug
performance considerably, while making the code much cleaner. On some
benchmarks, debug builds now run _much_ faster.
We no longer have to sprinkle our code with things like:
if(debugTagIsOn("context")) {
Debug("context") << theContext << std::endl;
}
which we had to do to get around performance problems previously.
Now just writing:
Debug("context") << theContext << std::endl;
does the same in production and debug builds. That is, if "context"
debugging is off, theContext isn't converted to a string, nor is it
output to a "/dev/null" ostream. I've confirmed this. In production
builds, the whole statement inlines to nothing. I've confirmed this
too.
Also, "Debug" is no longer a #definition, so you can use it directly
in production builds where you couldn't previously, e.g.
if(Debug.isOn("paranoid:check_tableau")) {
checkTableau();
}
I'm leaving debugTagIsOn() for now, but marking it as deprecated.
|
|
** file-level documentation at the top of the sources. **
This is the "make bugzilla stop bugging me" bugfix commit.
* Remove BackedNodeBuilder<> and collapse NodeBuilder<> hierarchy.
Updated documentation in the file. Resolves bug #99.
* Convenience NodeBuilders (PlusNodeBuilder, OrNodeBuilder, etc.)
moved into a separate file. Partially resolves bug #100.
* Moved isAssociative(Kind) into kind.h (and into the CVC4::kind
namespace) instead of metakind.h (where it was in CVC4::metakind).
This clears up a warning (private #inclusion) from the SMT and SMT2
parsers, and maybe makes more sense anyways, since this is based on
the kind (and not the metakind) of an operator.
* Documentation improvement; doxygen top-level \file gestures, \brief
gestures for files, etc. Changed contrib/update-copyright.pl for
this change, and post-processed to add \brief. Resolves bug #98.
* Removed ExprManager::mkExpr(Kind) and NodeManager::mkNode(Kind).
They no longer made sense. Resolves bug #91.
|
|
translation must indeed be a clause (if possible). I've changed the top level CNF conversion to generate clauses, instead of introducing unit clauses for each assertion.
|
|
To be done:
* Add erasable map Clause* to bool to minisat (backtracks with the solver)
* Add map from Clause* to Node (clauses that came from a node)
* Add reference counting Literal -> Node to CNFManager
* If Literal -> Node refcount goes to zero, the clauses of Node can be erased (if eresable)
* If clause is erased for each L in clause L -> Node refcount goes down
|
|
|
|
|
|
|
|
|
|
|
|
recognize an instantiation of the join conversion/copy ctor with
ref_count = ref_count_1 as a copy constructor. Problems with
reference counts ensue.
* src/theory/theory.h, src/theory/theory.cpp: Theory base
implementation work. Changed from continuation-style theory calls
to having an data member for the output channel. registerTerm() and
preRegisterTerm() work.
* src/theory/output_channel.h, src/theory/theory.h,
src/theory/theory.cpp, src/theory/uf/theory_uf.h,
src/theory/uf/theory_uf.cpp: merged ExplainOutputChannel into
OutputChannel.
* test/unit/expr/node_black.h: remove testPlusNode(),
testUMinusNode(), testMultNode().
* src/expr/attribute.h: new facilities ManagedAttribute<> and
CDAttribute<>, and add new template parameters to Attribute<>. Make
CDAttribute<>s work with context manager.
* src/expr/attribute.h, src/expr/node_manager.h: VarNameAttr and
TypeAttr are now "owned" (defined) by the NodeManager. The
AttributeManager knows nothing of specific attributes, it just as
all the code for dealing generically with attributes.
* test/unit/expr/node_white.h: test new attribute facilities.
* src/expr/soft_node.h: removed: We now have TNode, so SoftNode goes
away.
* src/theory/Makefile.am: fixed improper linking of theories
* src/theory/theory_engine.h: some implementation work (mainly stubs
for now, just to make sure TheoryUF can be instantiated properly,
etc.)
* src/expr/node_value.cpp, src/expr/node_value.h: move a number of
function implementations to the header and make them inline
* src/expr/node_manager.cpp, src/expr/node_manager.h: move a number of
function implementations to the header and make them inline
* src/theory/theoryof_table_prologue.h,
src/theory/theoryof_table_epilogue.h, src/theory/mktheoryof,
src/theory/Makefile.am: make the theoryOf() table from kinds and
implement TheoryEngine::theoryOf().
* src/theory/arith/Makefile, src/theory/bool/Makefile: generated these
stub Makefiles (with contrib/addsourcedir) as per policy
* src/theory/arith, src/theory/bool [directory properties]: add .deps
to svn:ignore.
* contrib/configure-in-place: permit configuring "in-place" in the
source directory.
* contrib/get-authors, contrib/dimacs_to_smt.pl,
contrib/update-copyright.pl, contrib/get-authors,
contrib/addsourcedir, src/expr/mkkind: copyright notice
* src/expr/node_manager.h, src/expr/node_builder.h,
src/prop/prop_engine.h, src/prop/prop_engine.cpp,
src/theory/theory_engine.h, src/smt/smt_engine.h, src/smt/smt_engine.cpp,
src/theory/output_channel.h: turn "const Node&"-typed formal
parameters into "TNode"
* src/theory/bool, src/theory/booleans: "bool" directory renamed "booleans"
to avoid keyword clash on containing namespace
* src/theory/booleans/theory_def.h, src/theory/uf/theory_def.h,
src/theory/arith/theory_def.h: "define" a theory simply (for automatic
theoryOf() generator).
* src/Makefile.am: build theory subdirectory before prop, smt, etc. so that
src/theory/theoryof_table.h header gets generated before it's needed
* src/expr/node_prologue.h, src/expr/node_middle.h: move "Kind" into a
separate CVC4::kind namespace to avoid its contents from cluttering
the CVC4 root namespace. Import the symbol "Kind" into the CVC4 namespace
but not the enum values.
* src/expr/node_manager.h, src/expr/node.h, src/expr/node_value.h,
src/expr/node_value.cpp, src/expr/expr.cpp, src/theory/uf/theory_uf.cpp,
src/prop/cnf_stream.cpp, src/parser/smt/smt_parser.g,
src/parser/cvc/cvc_parser.g, src/parser/antlr_parser.cpp,
test/unit/expr/node_white.h, test/unit/expr/node_black.h,
test/unit/expr/kind_black.h, test/unit/expr/node_builder_black.h:
update for having moved Kind into CVC4::kind.
* src/parser/parser.cpp: added file-does-not-exist check (was failing
silently).
|
|
* configure.ac, test/unit/Makefile.am: Resolved an issue where even
when not testing, one unit test was built.
* Re-ran contrib/update-copyright.pl on all source files to ensure
consistent and correct header comments.
* contrib/get-authors: Change definition of "minor contributor"
to >= 10% of lines (rather than strictly greater than 10% of lines)
|
|
and we're ready for nightly testing. We should not add regression tests that test future behaviour, as the builds will nag for all failing regressions. Thus, I've separated the multi-query regressions into multiple regressions until the cnf/context/sat is able to handle it. Also, fixed a typo in the CVC parser.
|
|
|
|
cvc4-c++-editing-mode from contrib/editing-with-emacs
|
|
|
|
Build src/expr before src/util.
Moved CVC4::Command to the expr package.
Re-quieted the "result is sat/invalid" etc. from PropEngine (this is
now done at the main driver level).
Added file-level documentation to Antlr sources
When built for debug, spin on SEGV instead of aborting. Really useful
for debugging problems that crop up only on long runs. Added
'--segv-nospin' to override this spinning so that "make check,"
nightly regressions, etc. don't hang when built with debug.
Updated src/main/about.h for 2010.
|
|
regenerated configure script
|
