| Age | Commit message (Collapse) | Author |
|---|
|
* added TheoryArith::preRewrite() to test and demonstrate
the use of pre-rewriting.
* array types and type checking now supported
* array type checking now supported
* theoryOf() dispatching properly to arrays now
* theories now required to implement a (simple) identify()
function that returns a string identifying them for
debugging/user output purposes
* added "builtin" theory to hold all built-in kinds and their
type rules and rewriting (currently only exploding distinct)
* fixed production build failure (regarding NodeSetDepth)
* removed an errant "using namespace std" in util/bitvector.h
(and made associated trivial fixes elsewhere)
* fixes to make unexpected exceptions more verbose in debug builds
* fixes to make multiple, cascading assertion fails simpler
* minor other fixes to comments etc.
|
|
|
|
expect a little turbulence. This commit will not compile. There will be a second commit that fixes this in a moment. I am delaying a change to avoid svn whining about a conflict.
|
|
documentation.
|
|
this Tuesday during the meeting. You'll need to run autogen and receonfigure after updating.
|
|
original){
|
|
|
|
|
|
|
|
|
|
call.
|
|
|
|
attribute. There is now a priority queue for selecting the smallest inconsistent basic variable. normal.h has been removed. A large chunk of the registerTerm() stuff has been moved into preregister. The lazy splitting code is now been commented out so that it stops showing up in profiling.
|
|
|
|
** 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.
|
|
assignment for slack variables once solving has begun. (They cannot just be 0.) The second has to do with how assignments are backttacked. Assignments are now tracked all of the time, and are frozen once they are known to be consistent, i.e. after a successful updateInconsistentVars(). Also added a fuzz test that shows both of these problems to the regressions.
|
|
|
|
debugging statements. There is some evidence that these debugging statements were 20% of the running time for QF_LRA/miplib/fixnet-1000.smt in debug mode.
|
|
before being used. Fixed a bug in node_builder.h's crop where a pointer is dereferenced after a realloc call.
|
|
the tableau now simulates older pivots while adding a new row.
|
|
false. This is temporary and will be removed once TheoryEngine rewriting is more fully debugged.
|
|
|
|
debugging utility that prints out the lower bound, upper bound, assignment, and the constraints that were asserted that caused the lower bound and upperbound to be asserted.
|
|
support has been added. Also a few bug fixes to Tableau.
|
|
|
|
rewriter.
|
|
Rational and Integer constructors are now explicit. This means that 'Integer = 3;' and so on are no longer permitted. This closes bug 121.
|
|
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
|
|
Real. See Bug 127 for a discussion of the hack. I am also adding a regression test that does not work (bug 128). It is not enabled so make check should still be fine.
|
|
TheoryArith. Also directly hacked in support for theoryOf() to work for equalities where the left hand is a variable of type real.
|
|
fixes and organizational changes. The theory is now enabled to perform checking in the TheoryEngine. This draft can now solve 2 new regression tests test/regress/regress0/ineq_slack.smt and test/regress/regress0/ineq_basic.smt. There is also a small bug fix inside src/expr/attribute.h.
|
|
|
|
|
|
This should not affect other parts of the system. This code is untested, and is volatile. It is going to be improved in the future so don't pick on it too much. I am merging this code in its current state back into the main trunk because it was getting unruly to keep merging the updated trunk back into the branch.
|
|
Also a bug fix to a couple of unit tests.
|
|
instead of assuming it's atomic based on kind. Atomicity is
determined at node building time. Fixes bug #81. If this is
determined to make node building too slow, we can allocate another
attribute "AtomicHasBeenComputed" to lazily compute atomicity.
* TheoryImpl<> has gone away. Theory implementations now derive from
Theory directly and share a single RegisteredAttr attribute for term
registration (which shouldn't overlap: every term is "owned" by
exactly one Theory). Fixes bug #79.
* Additional atomicity tests in ExprBlack unit test.
* More appropriate whitebox testing for attribute ID assignment
(AttributeWhite unit test).
* Better (and more correct) assertion checking in NodeBuilderBlack.
* run-regression script now checks exit status against what's provided
in "% EXIT: " gesture in .cvc input files, and stderr against
"% EXPECT-ERROR: ". These can be used to support intended failures.
Fixes bug #84. Also add "% EXIT: " gestures to all .cvc regressions
in repository.
* Solved some "control reaches end of non-void function" warnings in
src/parser/bounded_token_buffer.cpp by replacing
"AlwaysAssert(false)" with "Unreachable()" (which is known
statically to never return normally).
* Regression tests now use the cvc4 binary under
builds/$(CURRENT_BUILD)/src/main instead of the one in bin/ which
may not be properly installed yet at that point of the build.
(Partially fixes bug #46.)
* -fvisibility=hidden is now included by configure.ac instead of each
Makefile.am, which will make it easier to support platforms
(e.g. cygwin) that do things a different way.
* TheoryUF code formatting. (re: my code review bug #64)
* CDMap<> is leaking memory again, pending a fix for bug #85 in the
context subsystem. (To avoid serious errors, can't free context
objects.)
* add ContextWhite unit test for bug #85 (though it's currently
"defanged," awaiting the bugfix)
* Minor documentation, other cleanup.
|
|
* Other minor changes to the new parser to match coding guidelines,
add documentation, ....
* Add CFLAGS stuff to configure.ac parser Makefile.ams. This ensures
that profiling, coverage, optimization, debugging, and warning
level options will apply to the new parser as well (which is in C,
not C++). This fixes the deprecated warning we were seeing this
evening.
* Now, if you have ANTLR_HOME set in your environment, you don't need
to specify --with-antlr-dir to ./configure or have libantlr3c
installed in standard places. --with-antlr-dir still overrides
$ANTLR_HOME, and if the installation in $ANTLR_HOME is missing or
doesn't work, the standard places are still tried.
* Extend "silent make" to new parser stuff.
* Added src/parser/bounded_token_buffer.{h,cpp} to the list of
exclusions in contrib/update-copyright.pl and mention them as
excluded from CVC4 copyright in COPYING. They are antlr3-derived
works, covered under a BSD license.
OTHER STUFF:
* expr_manager.h, expr.h, expr_manager.cpp, and expr.cpp are now
auto-generated by a "mkexpr" script. This provides the correct
instantiations of mkConst() for public use, e.g., by the parser.
* Fix doxygen documentation in expr, expr_manager.. closes bug #35
* Node::isAtomic() implemented in a better way, based on theory kinds
files. Fixes bug #40. To support this, a "nonatomic_operator"
command has been added. All other "parameterized" or "operator"
kinds are atomic.
* Added expr_black test
* Remove kind::TRUE and kind::FALSE and make a new CONST_BOOLEAN kind
that takes a "bool" payload; for example, to make "true" you now do
nodeManager->mkConst(true).
* Make new "cvc4_public.h" and "cvc4parser_public.h" headers. Private
headers should include "cvc4_private.h"
(resp. "cvc4parser_private.h"), which existed previously. Public
headers should include the others. **No one** should include the
autoheader #include (which has been renamed "cvc4autoconfig.h")
directly, and public CVC4 headers can't access its #defines. This
is to avoid us having the same distribution problem as libantlr3c.
* Preliminary fixes based on Tim's code review of attributes (bug #61).
This includes splitting hairy template internals into
attribute_internals.h, for which another code review ticket will be
opened. Bug is still outstanding, but pending further
refactoring/documentation.
* Some *HashFcns renamed to *HashStrategy to match refactoring done
elsewhere (done by Chris?) earlier this week.
* Simplified creation of make rules for generated files (expr.cpp,
expr.h, expr_manager.cpp, expr_manager.h, theoryof_table.h, kind.h,
metakind.h).
* CVC4::Configuration interface and implementation split (so private
stuff doesn't leak into public headers).
* Some documentation/code formatting fixes.
* Add required versions of autotools to autogen.sh.
* src/expr/mkmetakind: fix a nonportable thing in invocation of "expr"
that was causing warnings on Red Hat.
* src/context/cdmap.h: add workaround to what appears to be a g++ 4.1
parsing bug.
|
|
|
|
|
|
* add NodeManagerWhite unit test
* change kind::APPLY to kind::APPLY_UF
* better APPLY handling: operators are no longer considered children
* more efficient pool lookup; the NodeValue doesn't have to be as fully constructed for the lookup to proceed
* extend DSL for kind declarations
+ new "theory" command declares a theory and its header. theory_def.h no longer required.
+ arity enforced on operators
+ constant mapping, hashing, equality
* CONSTANT metakinds supported (via Node::getConst<T>(), for example, Node::getConst<CVC4::Rational>() gets a Rational out of a Node (assuming it is of CONST_RATIONAL kind)
* added CONST_RATIONAL and CONST_INTEGER kinds
* builtin operators (AND, OR, PLUS, etc..) returned by Node::getOperator() are now CONSTANT metakind and are created by NodeManager
* Pretty-printing of Nodes now has a depth limit settable by a stream manipulator (e.g. "cout << Node::setdepth(5) << m << endl;" prints DAG rooted at m to a depth of 5)
* getters added to Node, TNode, NodeValue, etc., for operators and metakinds
* build-time generators for kind.h, metakind.h, and theoryof_table.h headers now have a simpler design and flag errors better, and the templates (kind_template.h etc.) are easier to understand.
* DISTINCT is now a kind, and the SMT parser now passes through DISTINCT nodes instead of blowing them up into ANDs. Until theory rewriting is online, though, DISTINCTs are directly blown up into conjunctions in TheoryEngine::rewrite().
* add gmpxx detection and inclusion
* better Asserts throughout, some documentation, cleanup
|
|
different "kinds of kinds" (special, operator, parameterized, and constant), and permits doxygen comments on them
|
|
policy discussion (no dead code, no unimplemented unit tests...), and
other fixes:
* src/expr/node_builder.h: uncomment AndNodeBuilder, OrNodeBuilder,
PlusNodeBuilder, and MultNodeBuilder. (These had been dead code for
awhile.)
* src/expr/node_value.cpp: toString() is much more reasonable now,
printing S-exprs and using variable names (instead of printing raw
pointer values). Next, we'll want to define a pretty-printing
theory interface and perhaps hook this up to that.
* test/unit/expr/node_black.h: implement testIterator(),
testToString(), and testToStream().
* test/unit/expr/node_builder_black.h: implement testIterator() and
testAppend(), and add some code to avoid the warnings on clear() for
unused NodeBuilders.
* src/expr/node_builder.h: redefine "iterator" to be over Nodes rather
than over NodeValues. Doesn't make sense to expose the underlying
NodeValues. This shouldn't affect anyone, no one was using
NodeBuilder iterators.
* fix some comments in source code
|
|
test behavior of grow(), which was previously very broken, fixed by
Tim earlier this afternoon.
* add the notion of a "private header". Private header files (those
not intended for distribution) should now #include "cvc4_private.h"
(or "cvc4parser_private.h" for the parser code). When not actually
building libcvc4 (resp. libcvc4parser), or associated unit tests, a
warning is emitted by the preprocessor. This should make it easier
to notice (and disentangle early) any unwanted public/private
mixing. Currently the warning identifies a couple places where we
need to fix things.
* added directory infrastructure for arrays and BV theories.
* the Theory inheritance hierarchy makes some assumptions about the
way inheritance is done. These are checked at runtime when
CVC4_ASSERTIONS is on. See src/theory/theory.h's TheoryImpl<>
definition for details.
* src/theory/booleans/theory_bool.h, src/theory/booleans/theory_def.h,
src/theory/arith/theory_arith.h, src/theory/arith/theory_def.h,
src/theory/uf/theory_uf.h, src/theory/uf/theory_def.h,
src/parser/antlr_parser.h: minor code formatting fixes as per
policy.
* src/theory/uf/theory_uf.cpp: fix for non-debug builds.
* src/util/options.h, src/util/model.h, src/util/result.h,
src/expr/type.h: make CVC4_PUBLIC.
* src/util/decision_engine.h: no longer CVC4_PUBLIC.
* src/expr/expr_manager.cpp: ExprManager::booleanType() and
ExprManager::kindType() weren't returning a value ?! Fixed.
* src/expr/expr_manager.h, src/expr/node_manager.h: ExprManager no
longer depends on NodeManager (public/private interface mixing).
ExprManagerScope is an internal implementation detail, and is moved
to node_manager.h.
* src/expr/node.h: mark gdb debug routines as "used" so that GCC
always emits code for them (even though its static analysis shows
they're unused).
|
|
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).
|
|
Updated contrib/update-copyright to handle Antlr (.g) parser/lexer inputs.
Updated copyright year.
Added a new "bool" theory (right now just to hold a kind.h contribution).
Added "kinds" files to UF and the new "bool" theory.
|
