diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-02 08:51:29 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-02 08:51:29 -0600 |
commit | 623e701247ed08e3f59d57b18ebe42f4d4db221e (patch) | |
tree | 663fa6451f9055a7256bd5c5ba4b558aeb58f46e /test/regress/regress0/fmf | |
parent | 9d6a0bda98ac2c3e3c59f55f349e029d623b264a (diff) |
Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and --fmf-fun-rlv, fixes bug 723.
Diffstat (limited to 'test/regress/regress0/fmf')
-rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/fmf/bug723-irrelevant-funs.smt2 | 52 |
2 files changed, 54 insertions, 1 deletions
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index cea0d7686..31fdb0a40 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -56,7 +56,8 @@ TESTS = \ agree466.smt2 \ LeftistHeap.scala-8-ncm.smt2 \ sc-crash-052316.smt2 \ - bound-int-alt.smt2 + bound-int-alt.smt2 \ + bug723-irrelevant-funs.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/bug723-irrelevant-funs.smt2 b/test/regress/regress0/fmf/bug723-irrelevant-funs.smt2 new file mode 100644 index 000000000..1a27bf170 --- /dev/null +++ b/test/regress/regress0/fmf/bug723-irrelevant-funs.smt2 @@ -0,0 +1,52 @@ +; COMMAND-LINE: --fmf-fun-rlv --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(define-fun $$isTrue$$ ((b Bool)) Bool b) +(define-fun $$isFalse$$ ((b Bool)) Bool (not b)) +(define-fun $$toString$$ ((b Bool)) String (ite b "true" "false") ) +(define-fun $$fromString$$ ((s String)) Bool (= s "true") ) +(define-fun $$inttostr$$ ((i Int)) String (ite (< i 0) (str.++ "-" (int.to.str (- i))) (int.to.str i))) +(declare-fun $$takeWhile$$ (String String) String) +(declare-fun $$takeWhileNot$$ (String String) String) +(declare-fun $$dropWhile$$ (String String) String) +(declare-fun $$dropWhileNot$$ (String String) String) +(declare-datatypes () ( + (AddressType (AddressType$C_AddressType (AddressType$C_AddressType$address String) (AddressType$C_AddressType$city String) (AddressType$C_AddressType$region String) (AddressType$C_AddressType$postalCode String) (AddressType$C_AddressType$country String))) + (Conditional_Int (Conditional_Int$CAbsent_Int) (Conditional_Int$CPresent_Int (Conditional_Int$CPresent_Int$value Int))) + (Conditional_dateTime (Conditional_dateTime$CAbsent_dateTime) (Conditional_dateTime$CPresent_dateTime (Conditional_dateTime$CPresent_dateTime$value Int))) + (Conditional_string (Conditional_string$CAbsent_string) (Conditional_string$CPresent_string (Conditional_string$CPresent_string$value String))) + (CustomerType (CustomerType$C_CustomerType (CustomerType$C_CustomerType$companyName String) (CustomerType$C_CustomerType$contactName String) (CustomerType$C_CustomerType$contactTitle String) (CustomerType$C_CustomerType$phone String) (CustomerType$C_CustomerType$fax Conditional_string) (CustomerType$C_CustomerType$fullAddress AddressType) (CustomerType$C_CustomerType$customerID Int))) + (List_CustomerType (List_CustomerType$CNil_CustomerType) (List_CustomerType$Cstr_CustomerType (List_CustomerType$Cstr_CustomerType$head CustomerType) (List_CustomerType$Cstr_CustomerType$tail List_CustomerType))) + (List_OrderType (List_OrderType$CNil_OrderType) (List_OrderType$Cstr_OrderType (List_OrderType$Cstr_OrderType$head OrderType) (List_OrderType$Cstr_OrderType$tail List_OrderType))) + (OrderType (OrderType$C_OrderType (OrderType$C_OrderType$customerID Int) (OrderType$C_OrderType$employeeID Int) (OrderType$C_OrderType$orderDate Int) (OrderType$C_OrderType$requiredDate Int) (OrderType$C_OrderType$shipInfo ShipInfoType))) + (RootType (RootType$C_RootType (RootType$C_RootType$customers List_CustomerType) (RootType$C_RootType$orders List_OrderType))) + (ShipInfoType (ShipInfoType$C_ShipInfoType (ShipInfoType$C_ShipInfoType$shipVia Int) (ShipInfoType$C_ShipInfoType$freight Int) (ShipInfoType$C_ShipInfoType$shipName String) (ShipInfoType$C_ShipInfoType$shipAddress String) (ShipInfoType$C_ShipInfoType$shipCity String) (ShipInfoType$C_ShipInfoType$shipRegion String) (ShipInfoType$C_ShipInfoType$shipPostalCode String) (ShipInfoType$C_ShipInfoType$shipCountry String) (ShipInfoType$C_ShipInfoType$shippedDate Conditional_dateTime))) +) ) + +(define-fun f2866$toXml((a$$2869 AddressType)) String (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "<FullAddress>" "<Address>") (AddressType$C_AddressType$address a$$2869)) "</Address>") "<City>") (AddressType$C_AddressType$city a$$2869)) "</City>") "<Region>") (AddressType$C_AddressType$region a$$2869)) "</Region>") "<PostalCode>") (AddressType$C_AddressType$postalCode a$$2869)) "</PostalCode>") "<Country>") (AddressType$C_AddressType$country a$$2869)) "</Country>") "</FullAddress>")) +(define-fun f2656$toXml((c$$2659 CustomerType)) String (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "<Customer CustomerID=" ($$inttostr$$ (CustomerType$C_CustomerType$customerID c$$2659))) ">") "<CompanyName>") (CustomerType$C_CustomerType$companyName c$$2659)) "</CompanyName>") "<ContactName>") (CustomerType$C_CustomerType$contactName c$$2659)) "</ContactName>") "<ContactTitle>") (CustomerType$C_CustomerType$contactTitle c$$2659)) "</ContactTitle>") "<Phone>") (CustomerType$C_CustomerType$phone c$$2659)) "</Phone>") (ite (is-Conditional_string$CPresent_string (CustomerType$C_CustomerType$fax c$$2659)) (str.++ (str.++ "<Fax>" (Conditional_string$CPresent_string$value (CustomerType$C_CustomerType$fax c$$2659))) "</Fax>") "")) (f2866$toXml (CustomerType$C_CustomerType$fullAddress c$$2659))) "</Customer>")) +(define-funs-rec + ( + (f2574$toXml((lc$$2577 List_CustomerType)) String) + ) + ( + (ite (is-List_CustomerType$CNil_CustomerType lc$$2577) "" (str.++ (f2656$toXml (List_CustomerType$Cstr_CustomerType$head lc$$2577)) (f2574$toXml (List_CustomerType$Cstr_CustomerType$tail lc$$2577)))) + ) +) +(define-fun f2942$toXml((s$$2945 ShipInfoType)) String (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "<ShipInfo" (ite (is-Conditional_dateTime$CPresent_dateTime (ShipInfoType$C_ShipInfoType$shippedDate s$$2945)) (str.++ (str.++ " ShippedDate=" ($$inttostr$$ (Conditional_dateTime$CPresent_dateTime$value (ShipInfoType$C_ShipInfoType$shippedDate s$$2945)))) ">") ">")) "<ShipVia>") ($$inttostr$$ (ShipInfoType$C_ShipInfoType$shipVia s$$2945))) "</ShipVia>") "<Freight>") ($$inttostr$$ (ShipInfoType$C_ShipInfoType$freight s$$2945))) "</Freight>") "<ShipName>") (ShipInfoType$C_ShipInfoType$shipName s$$2945)) "</ShipName>") "<ShipAddress>") (ShipInfoType$C_ShipInfoType$shipAddress s$$2945)) "</ShipAddress>") "<ShipCity>") (ShipInfoType$C_ShipInfoType$shipCity s$$2945)) "</ShipCity>") "<ShipRegion>") (ShipInfoType$C_ShipInfoType$shipRegion s$$2945)) "</ShipRegion>") "<ShipPostalCode>") (ShipInfoType$C_ShipInfoType$shipPostalCode s$$2945)) "</ShipPostalCode>") "<ShipCountry>") (ShipInfoType$C_ShipInfoType$shipCountry s$$2945)) "</ShipCountry>") "</ShipInfo>")) +(define-fun f2776$toXml((o$$2779 OrderType)) String (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "<Order>" "<CustomerID>") ($$inttostr$$ (OrderType$C_OrderType$customerID o$$2779))) "</CustomerID>") "<EmployeeID>") ($$inttostr$$ (OrderType$C_OrderType$employeeID o$$2779))) "</EmployeeID>") "<OrderDate>") ($$inttostr$$ (OrderType$C_OrderType$orderDate o$$2779))) "</OrderDate>") "<RequiredDate>") ($$inttostr$$ (OrderType$C_OrderType$requiredDate o$$2779))) "</RequiredDate>") (f2942$toXml (OrderType$C_OrderType$shipInfo o$$2779))) "</Order>")) +(define-funs-rec + ( + (f2615$toXml((lo$$2618 List_OrderType)) String) + ) + ( + (ite (is-List_OrderType$CNil_OrderType lo$$2618) "" (str.++ (f2776$toXml (List_OrderType$Cstr_OrderType$head lo$$2618)) (f2615$toXml (List_OrderType$Cstr_OrderType$tail lo$$2618)))) + ) +) +(define-fun f2526$toXml((r$$2529 RootType)) String (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "<Root>" "<Customers>") (f2574$toXml (RootType$C_RootType$customers r$$2529))) "</Customers>") "<Orders>") (f2615$toXml (RootType$C_RootType$orders r$$2529))) "</Orders>") "</Root>")) + +(declare-fun $Report$3105$0$1$() String) +(assert (= $Report$3105$0$1$ "<Root><Customers></Customers><Orders></Orders></Root>")) +; should be fast since functions introduced by define-fun-rec do not appear in the ground assertion +(check-sat) + |