diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-25 07:48:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-25 07:48:03 +0000 |
commit | 826f583ee14b922f39666dc827a5624fff753724 (patch) | |
tree | 03e7f1ad98b003dae5f6406bb990a715041d239c /src/parser/cvc | |
parent | f716b67e7bedd90c4dd43617158c0f55c1811334 (diff) |
* src/expr/node.h: add a copy constructor. Apparently GCC doesn't
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).
Diffstat (limited to 'src/parser/cvc')
-rw-r--r-- | src/parser/cvc/cvc_parser.g | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index bfdc4c0f2..9492b36d9 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -216,7 +216,7 @@ iffFormula returns [CVC4::Expr f] } : f = impliesFormula ( IFF e = iffFormula - { f = mkExpr(CVC4::IFF, f, e); } + { f = mkExpr(CVC4::kind::IFF, f, e); } )? ; @@ -230,7 +230,7 @@ impliesFormula returns [CVC4::Expr f] } : f = orFormula ( IMPLIES e = impliesFormula - { f = mkExpr(CVC4::IMPLIES, f, e); } + { f = mkExpr(CVC4::kind::IMPLIES, f, e); } )? ; @@ -246,7 +246,7 @@ orFormula returns [CVC4::Expr f] : e = xorFormula { exprs.push_back(e); } ( OR e = xorFormula { exprs.push_back(e); } )* { - f = (exprs.size() > 1 ? mkExpr(CVC4::OR, exprs) : exprs[0]); + f = (exprs.size() > 1 ? mkExpr(CVC4::kind::OR, exprs) : exprs[0]); } ; @@ -260,7 +260,7 @@ xorFormula returns [CVC4::Expr f] } : f = andFormula ( XOR e = andFormula - { f = mkExpr(CVC4::XOR,f, e); } + { f = mkExpr(CVC4::kind::XOR,f, e); } )* ; @@ -276,7 +276,7 @@ andFormula returns [CVC4::Expr f] : e = notFormula { exprs.push_back(e); } ( AND e = notFormula { exprs.push_back(e); } )* { - f = (exprs.size() > 1 ? mkExpr(CVC4::AND, exprs) : exprs[0]); + f = (exprs.size() > 1 ? mkExpr(CVC4::kind::AND, exprs) : exprs[0]); } ; @@ -290,7 +290,7 @@ notFormula returns [CVC4::Expr f] } : /* negation */ NOT f = notFormula - { f = mkExpr(CVC4::NOT, f); } + { f = mkExpr(CVC4::kind::NOT, f); } | /* a boolean atom */ f = predFormula ; @@ -302,7 +302,7 @@ predFormula returns [CVC4::Expr f] : { Expr e; } f = term (EQUAL e = term - { f = mkExpr(CVC4::EQUAL, f, e); } + { f = mkExpr(CVC4::kind::EQUAL, f, e); } )? ; // TODO: lt, gt, etc. @@ -323,7 +323,7 @@ term returns [CVC4::Expr t] LPAREN formulaList[args] RPAREN // TODO: check arity - { t = mkExpr(CVC4::APPLY, args); } + { t = mkExpr(CVC4::kind::APPLY, args); } | /* if-then-else */ t = iteTerm @@ -352,7 +352,7 @@ iteTerm returns [CVC4::Expr t] THEN iteThen = formula iteElse = iteElseTerm ENDIF - { t = mkExpr(CVC4::ITE, iteCondition, iteThen, iteElse); } + { t = mkExpr(CVC4::kind::ITE, iteCondition, iteThen, iteElse); } ; /** @@ -367,7 +367,7 @@ iteElseTerm returns [CVC4::Expr t] | ELSEIF iteCondition = formula THEN iteThen = formula iteElse = iteElseTerm - { t = mkExpr(CVC4::ITE, iteCondition, iteThen, iteElse); } + { t = mkExpr(CVC4::kind::ITE, iteCondition, iteThen, iteElse); } ; /** |