Fix TheoryAtom::term

potassco · Oct 20, 2023 · cf9f89b · cf9f89b
1 parent 7cd2fd3
commit cf9f89b
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 21 deletions.
diff --git a/src/ast_internals.rs b/src/ast_internals.rs
@@ -356,24 +356,13 @@ impl<'a> AST<'a> {
         Head { ast }
     }
     pub(crate) fn term(&self) -> Term {
-        let ast_type = self.get_type().unwrap();
-        dbg!(ast_type);
-        let ast_attr_type = self.get_attribute_type(ASTAttribute::Symbol).unwrap();
-        dbg!(ast_attr_type);
-        // TODO: This is a hack attribute should be ASTAttribute::Term
-        dbg!("Here is a hack attribute should be ASTAttribute::Term");
-        let ast = self.get_attribute_ast(ASTAttribute::Symbol).unwrap();
-        let ast_type = ast.get_type().unwrap();
-        dbg!(ast_type);
-        let ret = Function { ast };
-        let name = ret.to_string().unwrap();
-        dbg!(name);
-        ret.into()
+        let ast = self.get_attribute_ast(ASTAttribute::Term).unwrap();
+        Term { ast }
     }
     pub(crate) fn set_term(&mut self, term: Term) {
         let term = term.ast;
-        // TODO: This is a hack attribute should be ASTAttribute::Term
-        self.set_attribute_ast(ASTAttribute::Symbol, term).unwrap();
+        // TODO: check
+        self.set_attribute_ast(ASTAttribute::Term, term).unwrap();
     }
     pub(crate) fn guard(&self) -> TheoryGuard {
         // TODO: check

diff --git a/tests/integration_test.rs b/tests/integration_test.rs
@@ -280,9 +280,12 @@ fn ast_literal() {
 fn ast_head_literal() {
     let loc = Location::default();
     let sym = Symbol::create_id("test", true).unwrap();
+    let sym2 = Symbol::create_id("toast", true).unwrap();
+    let sym3 = Symbol::create_id("tset", true).unwrap();
     let term1 = symbolic_term(&loc, &sym).unwrap();
+    let term2 = symbolic_term(&loc, &sym2).unwrap();
+    let term3 = symbolic_term(&loc, &sym3).unwrap();
     let atom1 = symbolic_atom(term1.clone()).unwrap();
-    let term2 = symbolic_term(&loc, &sym).unwrap();
     let atom2 = symbolic_atom(term2).unwrap();
     let lit = basic_literal_from_symbolic_atom(&loc, Sign::NoSign, atom1).unwrap();
     let lit2 = basic_literal_from_symbolic_atom(&loc, Sign::NoSign, atom2).unwrap();
@@ -300,22 +303,30 @@ fn ast_head_literal() {
     let element = theory_atom_element(&tuple, &condition).unwrap();
     let elements = [element];
     let guard = theory_guard("theory_operator", term1.clone()).unwrap();
-    let tatom = theory_atom(&loc, term1, &elements, Some(guard)).unwrap();
+    let tatom = theory_atom(&loc, term3, &elements, Some(guard)).unwrap();
 
     let hlit: ast::Head = lit.into();
     assert_eq!(format!("{}", hlit), "test");
 
     let hlit: ast::Head = dis.into();
-    assert_eq!(format!("{}", hlit), "test: test");
+    assert_eq!(format!("{}", hlit), "test: toast");
 
     let hlit: Head = hagg.into();
-    assert_eq!(format!("{}", hlit), "#count { test: test: test }");
+    assert_eq!(format!("{}", hlit), "#count { test: test: toast }");
 
-    let hlit: Head = tatom.into();
+    let hlit: Head = tatom.clone().into();
     assert_eq!(
         format!("{}", hlit),
-        "&test { test: test } theory_operator test"
+        "&tset { test: toast } theory_operator test"
     );
+
+    let ta_term : Term = tatom.term();
+    assert_eq!(
+        format!("{}", ta_term),
+        "tset"
+    );
+
+
 }
 #[test]
 fn ast_body_literal() {